Step | Hyp | Ref
| Expression |
1 | | mplsubglem.s |
. . 3
⊢ 𝑆 = (𝐼 mPwSer 𝑅) |
2 | | mplsubglem.i |
. . 3
⊢ (𝜑 → 𝐼 ∈ 𝑊) |
3 | | mpllsslem.r |
. . 3
⊢ (𝜑 → 𝑅 ∈ Ring) |
4 | 1, 2, 3 | psrsca 19210 |
. 2
⊢ (𝜑 → 𝑅 = (Scalar‘𝑆)) |
5 | | eqidd 2611 |
. 2
⊢ (𝜑 → (Base‘𝑅) = (Base‘𝑅)) |
6 | | mplsubglem.b |
. . 3
⊢ 𝐵 = (Base‘𝑆) |
7 | 6 | a1i 11 |
. 2
⊢ (𝜑 → 𝐵 = (Base‘𝑆)) |
8 | | eqidd 2611 |
. 2
⊢ (𝜑 → (+g‘𝑆) = (+g‘𝑆)) |
9 | | eqidd 2611 |
. 2
⊢ (𝜑 → (
·𝑠 ‘𝑆) = ( ·𝑠
‘𝑆)) |
10 | | eqidd 2611 |
. 2
⊢ (𝜑 → (LSubSp‘𝑆) = (LSubSp‘𝑆)) |
11 | | mplsubglem.z |
. . . 4
⊢ 0 =
(0g‘𝑅) |
12 | | mplsubglem.d |
. . . 4
⊢ 𝐷 = {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈
Fin} |
13 | | mplsubglem.0 |
. . . 4
⊢ (𝜑 → ∅ ∈ 𝐴) |
14 | | mplsubglem.a |
. . . 4
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴)) → (𝑥 ∪ 𝑦) ∈ 𝐴) |
15 | | mplsubglem.y |
. . . 4
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ⊆ 𝑥)) → 𝑦 ∈ 𝐴) |
16 | | mplsubglem.u |
. . . 4
⊢ (𝜑 → 𝑈 = {𝑔 ∈ 𝐵 ∣ (𝑔 supp 0 ) ∈ 𝐴}) |
17 | | ringgrp 18375 |
. . . . 5
⊢ (𝑅 ∈ Ring → 𝑅 ∈ Grp) |
18 | 3, 17 | syl 17 |
. . . 4
⊢ (𝜑 → 𝑅 ∈ Grp) |
19 | 1, 6, 11, 12, 2, 13, 14, 15, 16, 18 | mplsubglem 19255 |
. . 3
⊢ (𝜑 → 𝑈 ∈ (SubGrp‘𝑆)) |
20 | 6 | subgss 17418 |
. . 3
⊢ (𝑈 ∈ (SubGrp‘𝑆) → 𝑈 ⊆ 𝐵) |
21 | 19, 20 | syl 17 |
. 2
⊢ (𝜑 → 𝑈 ⊆ 𝐵) |
22 | | eqid 2610 |
. . . 4
⊢
(0g‘𝑆) = (0g‘𝑆) |
23 | 22 | subg0cl 17425 |
. . 3
⊢ (𝑈 ∈ (SubGrp‘𝑆) →
(0g‘𝑆)
∈ 𝑈) |
24 | | ne0i 3880 |
. . 3
⊢
((0g‘𝑆) ∈ 𝑈 → 𝑈 ≠ ∅) |
25 | 19, 23, 24 | 3syl 18 |
. 2
⊢ (𝜑 → 𝑈 ≠ ∅) |
26 | 19 | adantr 480 |
. . 3
⊢ ((𝜑 ∧ (𝑢 ∈ (Base‘𝑅) ∧ 𝑣 ∈ 𝑈 ∧ 𝑤 ∈ 𝑈)) → 𝑈 ∈ (SubGrp‘𝑆)) |
27 | | eqid 2610 |
. . . . . 6
⊢ (
·𝑠 ‘𝑆) = ( ·𝑠
‘𝑆) |
28 | | eqid 2610 |
. . . . . 6
⊢
(Base‘𝑅) =
(Base‘𝑅) |
29 | 3 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑢 ∈ (Base‘𝑅) ∧ 𝑣 ∈ 𝑈)) → 𝑅 ∈ Ring) |
30 | | simprl 790 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑢 ∈ (Base‘𝑅) ∧ 𝑣 ∈ 𝑈)) → 𝑢 ∈ (Base‘𝑅)) |
31 | | simprr 792 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑢 ∈ (Base‘𝑅) ∧ 𝑣 ∈ 𝑈)) → 𝑣 ∈ 𝑈) |
32 | 16 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑢 ∈ (Base‘𝑅) ∧ 𝑣 ∈ 𝑈)) → 𝑈 = {𝑔 ∈ 𝐵 ∣ (𝑔 supp 0 ) ∈ 𝐴}) |
33 | 32 | eleq2d 2673 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑢 ∈ (Base‘𝑅) ∧ 𝑣 ∈ 𝑈)) → (𝑣 ∈ 𝑈 ↔ 𝑣 ∈ {𝑔 ∈ 𝐵 ∣ (𝑔 supp 0 ) ∈ 𝐴})) |
34 | | oveq1 6556 |
. . . . . . . . . . 11
⊢ (𝑔 = 𝑣 → (𝑔 supp 0 ) = (𝑣 supp 0 )) |
35 | 34 | eleq1d 2672 |
. . . . . . . . . 10
⊢ (𝑔 = 𝑣 → ((𝑔 supp 0 ) ∈ 𝐴 ↔ (𝑣 supp 0 ) ∈ 𝐴)) |
36 | 35 | elrab 3331 |
. . . . . . . . 9
⊢ (𝑣 ∈ {𝑔 ∈ 𝐵 ∣ (𝑔 supp 0 ) ∈ 𝐴} ↔ (𝑣 ∈ 𝐵 ∧ (𝑣 supp 0 ) ∈ 𝐴)) |
37 | 33, 36 | syl6bb 275 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑢 ∈ (Base‘𝑅) ∧ 𝑣 ∈ 𝑈)) → (𝑣 ∈ 𝑈 ↔ (𝑣 ∈ 𝐵 ∧ (𝑣 supp 0 ) ∈ 𝐴))) |
38 | 31, 37 | mpbid 221 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑢 ∈ (Base‘𝑅) ∧ 𝑣 ∈ 𝑈)) → (𝑣 ∈ 𝐵 ∧ (𝑣 supp 0 ) ∈ 𝐴)) |
39 | 38 | simpld 474 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑢 ∈ (Base‘𝑅) ∧ 𝑣 ∈ 𝑈)) → 𝑣 ∈ 𝐵) |
40 | 1, 27, 28, 6, 29, 30, 39 | psrvscacl 19214 |
. . . . 5
⊢ ((𝜑 ∧ (𝑢 ∈ (Base‘𝑅) ∧ 𝑣 ∈ 𝑈)) → (𝑢( ·𝑠
‘𝑆)𝑣) ∈ 𝐵) |
41 | | ovex 6577 |
. . . . . . 7
⊢ ((𝑢(
·𝑠 ‘𝑆)𝑣) supp 0 ) ∈
V |
42 | 41 | a1i 11 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑢 ∈ (Base‘𝑅) ∧ 𝑣 ∈ 𝑈)) → ((𝑢( ·𝑠
‘𝑆)𝑣) supp 0 ) ∈
V) |
43 | 38 | simprd 478 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑢 ∈ (Base‘𝑅) ∧ 𝑣 ∈ 𝑈)) → (𝑣 supp 0 ) ∈ 𝐴) |
44 | 15 | expr 641 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝑦 ⊆ 𝑥 → 𝑦 ∈ 𝐴)) |
45 | 44 | alrimiv 1842 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ∀𝑦(𝑦 ⊆ 𝑥 → 𝑦 ∈ 𝐴)) |
46 | 45 | ralrimiva 2949 |
. . . . . . . 8
⊢ (𝜑 → ∀𝑥 ∈ 𝐴 ∀𝑦(𝑦 ⊆ 𝑥 → 𝑦 ∈ 𝐴)) |
47 | 46 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑢 ∈ (Base‘𝑅) ∧ 𝑣 ∈ 𝑈)) → ∀𝑥 ∈ 𝐴 ∀𝑦(𝑦 ⊆ 𝑥 → 𝑦 ∈ 𝐴)) |
48 | | sseq2 3590 |
. . . . . . . . . 10
⊢ (𝑥 = (𝑣 supp 0 ) → (𝑦 ⊆ 𝑥 ↔ 𝑦 ⊆ (𝑣 supp 0 ))) |
49 | 48 | imbi1d 330 |
. . . . . . . . 9
⊢ (𝑥 = (𝑣 supp 0 ) → ((𝑦 ⊆ 𝑥 → 𝑦 ∈ 𝐴) ↔ (𝑦 ⊆ (𝑣 supp 0 ) → 𝑦 ∈ 𝐴))) |
50 | 49 | albidv 1836 |
. . . . . . . 8
⊢ (𝑥 = (𝑣 supp 0 ) → (∀𝑦(𝑦 ⊆ 𝑥 → 𝑦 ∈ 𝐴) ↔ ∀𝑦(𝑦 ⊆ (𝑣 supp 0 ) → 𝑦 ∈ 𝐴))) |
51 | 50 | rspcv 3278 |
. . . . . . 7
⊢ ((𝑣 supp 0 ) ∈ 𝐴 → (∀𝑥 ∈ 𝐴 ∀𝑦(𝑦 ⊆ 𝑥 → 𝑦 ∈ 𝐴) → ∀𝑦(𝑦 ⊆ (𝑣 supp 0 ) → 𝑦 ∈ 𝐴))) |
52 | 43, 47, 51 | sylc 63 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑢 ∈ (Base‘𝑅) ∧ 𝑣 ∈ 𝑈)) → ∀𝑦(𝑦 ⊆ (𝑣 supp 0 ) → 𝑦 ∈ 𝐴)) |
53 | 1, 28, 12, 6, 40 | psrelbas 19200 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑢 ∈ (Base‘𝑅) ∧ 𝑣 ∈ 𝑈)) → (𝑢( ·𝑠
‘𝑆)𝑣):𝐷⟶(Base‘𝑅)) |
54 | | eqid 2610 |
. . . . . . . . 9
⊢
(.r‘𝑅) = (.r‘𝑅) |
55 | 30 | adantr 480 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑢 ∈ (Base‘𝑅) ∧ 𝑣 ∈ 𝑈)) ∧ 𝑘 ∈ (𝐷 ∖ (𝑣 supp 0 ))) → 𝑢 ∈ (Base‘𝑅)) |
56 | 39 | adantr 480 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑢 ∈ (Base‘𝑅) ∧ 𝑣 ∈ 𝑈)) ∧ 𝑘 ∈ (𝐷 ∖ (𝑣 supp 0 ))) → 𝑣 ∈ 𝐵) |
57 | | eldifi 3694 |
. . . . . . . . . 10
⊢ (𝑘 ∈ (𝐷 ∖ (𝑣 supp 0 )) → 𝑘 ∈ 𝐷) |
58 | 57 | adantl 481 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑢 ∈ (Base‘𝑅) ∧ 𝑣 ∈ 𝑈)) ∧ 𝑘 ∈ (𝐷 ∖ (𝑣 supp 0 ))) → 𝑘 ∈ 𝐷) |
59 | 1, 27, 28, 6, 54, 12, 55, 56, 58 | psrvscaval 19213 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑢 ∈ (Base‘𝑅) ∧ 𝑣 ∈ 𝑈)) ∧ 𝑘 ∈ (𝐷 ∖ (𝑣 supp 0 ))) → ((𝑢(
·𝑠 ‘𝑆)𝑣)‘𝑘) = (𝑢(.r‘𝑅)(𝑣‘𝑘))) |
60 | 1, 28, 12, 6, 39 | psrelbas 19200 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑢 ∈ (Base‘𝑅) ∧ 𝑣 ∈ 𝑈)) → 𝑣:𝐷⟶(Base‘𝑅)) |
61 | | ssid 3587 |
. . . . . . . . . . 11
⊢ (𝑣 supp 0 ) ⊆ (𝑣 supp 0 ) |
62 | 61 | a1i 11 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑢 ∈ (Base‘𝑅) ∧ 𝑣 ∈ 𝑈)) → (𝑣 supp 0 ) ⊆ (𝑣 supp 0 )) |
63 | | ovex 6577 |
. . . . . . . . . . . 12
⊢
(ℕ0 ↑𝑚 𝐼) ∈ V |
64 | 12, 63 | rabex2 4742 |
. . . . . . . . . . 11
⊢ 𝐷 ∈ V |
65 | 64 | a1i 11 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑢 ∈ (Base‘𝑅) ∧ 𝑣 ∈ 𝑈)) → 𝐷 ∈ V) |
66 | | fvex 6113 |
. . . . . . . . . . . 12
⊢
(0g‘𝑅) ∈ V |
67 | 11, 66 | eqeltri 2684 |
. . . . . . . . . . 11
⊢ 0 ∈
V |
68 | 67 | a1i 11 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑢 ∈ (Base‘𝑅) ∧ 𝑣 ∈ 𝑈)) → 0 ∈ V) |
69 | 60, 62, 65, 68 | suppssr 7213 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑢 ∈ (Base‘𝑅) ∧ 𝑣 ∈ 𝑈)) ∧ 𝑘 ∈ (𝐷 ∖ (𝑣 supp 0 ))) → (𝑣‘𝑘) = 0 ) |
70 | 69 | oveq2d 6565 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑢 ∈ (Base‘𝑅) ∧ 𝑣 ∈ 𝑈)) ∧ 𝑘 ∈ (𝐷 ∖ (𝑣 supp 0 ))) → (𝑢(.r‘𝑅)(𝑣‘𝑘)) = (𝑢(.r‘𝑅) 0 )) |
71 | 28, 54, 11 | ringrz 18411 |
. . . . . . . . . 10
⊢ ((𝑅 ∈ Ring ∧ 𝑢 ∈ (Base‘𝑅)) → (𝑢(.r‘𝑅) 0 ) = 0 ) |
72 | 3, 30, 71 | syl2an2r 872 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑢 ∈ (Base‘𝑅) ∧ 𝑣 ∈ 𝑈)) → (𝑢(.r‘𝑅) 0 ) = 0 ) |
73 | 72 | adantr 480 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑢 ∈ (Base‘𝑅) ∧ 𝑣 ∈ 𝑈)) ∧ 𝑘 ∈ (𝐷 ∖ (𝑣 supp 0 ))) → (𝑢(.r‘𝑅) 0 ) = 0 ) |
74 | 59, 70, 73 | 3eqtrd 2648 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑢 ∈ (Base‘𝑅) ∧ 𝑣 ∈ 𝑈)) ∧ 𝑘 ∈ (𝐷 ∖ (𝑣 supp 0 ))) → ((𝑢(
·𝑠 ‘𝑆)𝑣)‘𝑘) = 0 ) |
75 | 53, 74 | suppss 7212 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑢 ∈ (Base‘𝑅) ∧ 𝑣 ∈ 𝑈)) → ((𝑢( ·𝑠
‘𝑆)𝑣) supp 0 ) ⊆ (𝑣 supp 0 )) |
76 | | sseq1 3589 |
. . . . . . . 8
⊢ (𝑦 = ((𝑢( ·𝑠
‘𝑆)𝑣) supp 0 ) → (𝑦 ⊆ (𝑣 supp 0 ) ↔ ((𝑢(
·𝑠 ‘𝑆)𝑣) supp 0 ) ⊆ (𝑣 supp 0 ))) |
77 | | eleq1 2676 |
. . . . . . . 8
⊢ (𝑦 = ((𝑢( ·𝑠
‘𝑆)𝑣) supp 0 ) → (𝑦 ∈ 𝐴 ↔ ((𝑢( ·𝑠
‘𝑆)𝑣) supp 0 ) ∈ 𝐴)) |
78 | 76, 77 | imbi12d 333 |
. . . . . . 7
⊢ (𝑦 = ((𝑢( ·𝑠
‘𝑆)𝑣) supp 0 ) → ((𝑦 ⊆ (𝑣 supp 0 ) → 𝑦 ∈ 𝐴) ↔ (((𝑢( ·𝑠
‘𝑆)𝑣) supp 0 ) ⊆ (𝑣 supp 0 ) → ((𝑢(
·𝑠 ‘𝑆)𝑣) supp 0 ) ∈ 𝐴))) |
79 | 78 | spcgv 3266 |
. . . . . 6
⊢ (((𝑢(
·𝑠 ‘𝑆)𝑣) supp 0 ) ∈ V →
(∀𝑦(𝑦 ⊆ (𝑣 supp 0 ) → 𝑦 ∈ 𝐴) → (((𝑢( ·𝑠
‘𝑆)𝑣) supp 0 ) ⊆ (𝑣 supp 0 ) → ((𝑢(
·𝑠 ‘𝑆)𝑣) supp 0 ) ∈ 𝐴))) |
80 | 42, 52, 75, 79 | syl3c 64 |
. . . . 5
⊢ ((𝜑 ∧ (𝑢 ∈ (Base‘𝑅) ∧ 𝑣 ∈ 𝑈)) → ((𝑢( ·𝑠
‘𝑆)𝑣) supp 0 ) ∈ 𝐴) |
81 | 32 | eleq2d 2673 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑢 ∈ (Base‘𝑅) ∧ 𝑣 ∈ 𝑈)) → ((𝑢( ·𝑠
‘𝑆)𝑣) ∈ 𝑈 ↔ (𝑢( ·𝑠
‘𝑆)𝑣) ∈ {𝑔 ∈ 𝐵 ∣ (𝑔 supp 0 ) ∈ 𝐴})) |
82 | | oveq1 6556 |
. . . . . . . 8
⊢ (𝑔 = (𝑢( ·𝑠
‘𝑆)𝑣) → (𝑔 supp 0 ) = ((𝑢( ·𝑠
‘𝑆)𝑣) supp 0 )) |
83 | 82 | eleq1d 2672 |
. . . . . . 7
⊢ (𝑔 = (𝑢( ·𝑠
‘𝑆)𝑣) → ((𝑔 supp 0 ) ∈ 𝐴 ↔ ((𝑢( ·𝑠
‘𝑆)𝑣) supp 0 ) ∈ 𝐴)) |
84 | 83 | elrab 3331 |
. . . . . 6
⊢ ((𝑢(
·𝑠 ‘𝑆)𝑣) ∈ {𝑔 ∈ 𝐵 ∣ (𝑔 supp 0 ) ∈ 𝐴} ↔ ((𝑢( ·𝑠
‘𝑆)𝑣) ∈ 𝐵 ∧ ((𝑢( ·𝑠
‘𝑆)𝑣) supp 0 ) ∈ 𝐴)) |
85 | 81, 84 | syl6bb 275 |
. . . . 5
⊢ ((𝜑 ∧ (𝑢 ∈ (Base‘𝑅) ∧ 𝑣 ∈ 𝑈)) → ((𝑢( ·𝑠
‘𝑆)𝑣) ∈ 𝑈 ↔ ((𝑢( ·𝑠
‘𝑆)𝑣) ∈ 𝐵 ∧ ((𝑢( ·𝑠
‘𝑆)𝑣) supp 0 ) ∈ 𝐴))) |
86 | 40, 80, 85 | mpbir2and 959 |
. . . 4
⊢ ((𝜑 ∧ (𝑢 ∈ (Base‘𝑅) ∧ 𝑣 ∈ 𝑈)) → (𝑢( ·𝑠
‘𝑆)𝑣) ∈ 𝑈) |
87 | 86 | 3adantr3 1215 |
. . 3
⊢ ((𝜑 ∧ (𝑢 ∈ (Base‘𝑅) ∧ 𝑣 ∈ 𝑈 ∧ 𝑤 ∈ 𝑈)) → (𝑢( ·𝑠
‘𝑆)𝑣) ∈ 𝑈) |
88 | | simpr3 1062 |
. . 3
⊢ ((𝜑 ∧ (𝑢 ∈ (Base‘𝑅) ∧ 𝑣 ∈ 𝑈 ∧ 𝑤 ∈ 𝑈)) → 𝑤 ∈ 𝑈) |
89 | | eqid 2610 |
. . . 4
⊢
(+g‘𝑆) = (+g‘𝑆) |
90 | 89 | subgcl 17427 |
. . 3
⊢ ((𝑈 ∈ (SubGrp‘𝑆) ∧ (𝑢( ·𝑠
‘𝑆)𝑣) ∈ 𝑈 ∧ 𝑤 ∈ 𝑈) → ((𝑢( ·𝑠
‘𝑆)𝑣)(+g‘𝑆)𝑤) ∈ 𝑈) |
91 | 26, 87, 88, 90 | syl3anc 1318 |
. 2
⊢ ((𝜑 ∧ (𝑢 ∈ (Base‘𝑅) ∧ 𝑣 ∈ 𝑈 ∧ 𝑤 ∈ 𝑈)) → ((𝑢( ·𝑠
‘𝑆)𝑣)(+g‘𝑆)𝑤) ∈ 𝑈) |
92 | 4, 5, 7, 8, 9, 10,
21, 25, 91 | islssd 18757 |
1
⊢ (𝜑 → 𝑈 ∈ (LSubSp‘𝑆)) |