Step | Hyp | Ref
| Expression |
1 | | mplsubglem.u |
. . 3
⊢ (𝜑 → 𝑈 = {𝑔 ∈ 𝐵 ∣ (𝑔 supp 0 ) ∈ 𝐴}) |
2 | | ssrab2 3908 |
. . 3
⊢ {𝑔 ∈ 𝐵 ∣ (𝑔 supp 0 ) ∈ 𝐴} ⊆ 𝐵 |
3 | 1, 2 | syl6eqss 3874 |
. 2
⊢ (𝜑 → 𝑈 ⊆ 𝐵) |
4 | | mplsubglem.s |
. . . . 5
⊢ 𝑆 = (𝐼 mPwSer 𝑅) |
5 | | mplsubglem.i |
. . . . 5
⊢ (𝜑 → 𝐼 ∈ 𝑊) |
6 | | mplsubglem.r |
. . . . 5
⊢ (𝜑 → 𝑅 ∈ Grp) |
7 | | mplsubglem.d |
. . . . 5
⊢ 𝐷 = {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈
Fin} |
8 | | mplsubglem.z |
. . . . 5
⊢ 0 =
(0g‘𝑅) |
9 | | mplsubglem.b |
. . . . 5
⊢ 𝐵 = (Base‘𝑆) |
10 | 4, 5, 6, 7, 8, 9 | psr0cl 19795 |
. . . 4
⊢ (𝜑 → (𝐷 × { 0 }) ∈ 𝐵) |
11 | | eqid 2778 |
. . . . . . . . 9
⊢
(Base‘𝑅) =
(Base‘𝑅) |
12 | 11, 8 | grpidcl 17841 |
. . . . . . . 8
⊢ (𝑅 ∈ Grp → 0 ∈
(Base‘𝑅)) |
13 | | fconst6g 6346 |
. . . . . . . 8
⊢ ( 0 ∈
(Base‘𝑅) →
(𝐷 × { 0 }):𝐷⟶(Base‘𝑅)) |
14 | 6, 12, 13 | 3syl 18 |
. . . . . . 7
⊢ (𝜑 → (𝐷 × { 0 }):𝐷⟶(Base‘𝑅)) |
15 | | eldifi 3955 |
. . . . . . . . 9
⊢ (𝑢 ∈ (𝐷 ∖ ∅) → 𝑢 ∈ 𝐷) |
16 | 8 | fvexi 6462 |
. . . . . . . . . 10
⊢ 0 ∈
V |
17 | 16 | fvconst2 6743 |
. . . . . . . . 9
⊢ (𝑢 ∈ 𝐷 → ((𝐷 × { 0 })‘𝑢) = 0 ) |
18 | 15, 17 | syl 17 |
. . . . . . . 8
⊢ (𝑢 ∈ (𝐷 ∖ ∅) → ((𝐷 × { 0 })‘𝑢) = 0 ) |
19 | 18 | adantl 475 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑢 ∈ (𝐷 ∖ ∅)) → ((𝐷 × { 0 })‘𝑢) = 0 ) |
20 | 14, 19 | suppss 7609 |
. . . . . 6
⊢ (𝜑 → ((𝐷 × { 0 }) supp 0 ) ⊆
∅) |
21 | | ss0 4200 |
. . . . . 6
⊢ (((𝐷 × { 0 }) supp 0 ) ⊆ ∅ →
((𝐷 × { 0 }) supp 0 ) =
∅) |
22 | 20, 21 | syl 17 |
. . . . 5
⊢ (𝜑 → ((𝐷 × { 0 }) supp 0 ) =
∅) |
23 | | mplsubglem.0 |
. . . . 5
⊢ (𝜑 → ∅ ∈ 𝐴) |
24 | 22, 23 | eqeltrd 2859 |
. . . 4
⊢ (𝜑 → ((𝐷 × { 0 }) supp 0 ) ∈ 𝐴) |
25 | 1 | eleq2d 2845 |
. . . . 5
⊢ (𝜑 → ((𝐷 × { 0 }) ∈ 𝑈 ↔ (𝐷 × { 0 }) ∈ {𝑔 ∈ 𝐵 ∣ (𝑔 supp 0 ) ∈ 𝐴})) |
26 | | oveq1 6931 |
. . . . . . 7
⊢ (𝑔 = (𝐷 × { 0 }) → (𝑔 supp 0 ) = ((𝐷 × { 0 }) supp 0 )) |
27 | 26 | eleq1d 2844 |
. . . . . 6
⊢ (𝑔 = (𝐷 × { 0 }) → ((𝑔 supp 0 ) ∈ 𝐴 ↔ ((𝐷 × { 0 }) supp 0 ) ∈ 𝐴)) |
28 | 27 | elrab 3572 |
. . . . 5
⊢ ((𝐷 × { 0 }) ∈ {𝑔 ∈ 𝐵 ∣ (𝑔 supp 0 ) ∈ 𝐴} ↔ ((𝐷 × { 0 }) ∈ 𝐵 ∧ ((𝐷 × { 0 }) supp 0 ) ∈ 𝐴)) |
29 | 25, 28 | syl6bb 279 |
. . . 4
⊢ (𝜑 → ((𝐷 × { 0 }) ∈ 𝑈 ↔ ((𝐷 × { 0 }) ∈ 𝐵 ∧ ((𝐷 × { 0 }) supp 0 ) ∈ 𝐴))) |
30 | 10, 24, 29 | mpbir2and 703 |
. . 3
⊢ (𝜑 → (𝐷 × { 0 }) ∈ 𝑈) |
31 | 30 | ne0d 4150 |
. 2
⊢ (𝜑 → 𝑈 ≠ ∅) |
32 | | eqid 2778 |
. . . . . . 7
⊢
(+g‘𝑆) = (+g‘𝑆) |
33 | 6 | ad2antrr 716 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) → 𝑅 ∈ Grp) |
34 | 1 | eleq2d 2845 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑢 ∈ 𝑈 ↔ 𝑢 ∈ {𝑔 ∈ 𝐵 ∣ (𝑔 supp 0 ) ∈ 𝐴})) |
35 | | oveq1 6931 |
. . . . . . . . . . . . 13
⊢ (𝑔 = 𝑢 → (𝑔 supp 0 ) = (𝑢 supp 0 )) |
36 | 35 | eleq1d 2844 |
. . . . . . . . . . . 12
⊢ (𝑔 = 𝑢 → ((𝑔 supp 0 ) ∈ 𝐴 ↔ (𝑢 supp 0 ) ∈ 𝐴)) |
37 | 36 | elrab 3572 |
. . . . . . . . . . 11
⊢ (𝑢 ∈ {𝑔 ∈ 𝐵 ∣ (𝑔 supp 0 ) ∈ 𝐴} ↔ (𝑢 ∈ 𝐵 ∧ (𝑢 supp 0 ) ∈ 𝐴)) |
38 | 34, 37 | syl6bb 279 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑢 ∈ 𝑈 ↔ (𝑢 ∈ 𝐵 ∧ (𝑢 supp 0 ) ∈ 𝐴))) |
39 | 38 | biimpa 470 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑢 ∈ 𝑈) → (𝑢 ∈ 𝐵 ∧ (𝑢 supp 0 ) ∈ 𝐴)) |
40 | 39 | simpld 490 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑢 ∈ 𝑈) → 𝑢 ∈ 𝐵) |
41 | 40 | adantr 474 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) → 𝑢 ∈ 𝐵) |
42 | 1 | adantr 474 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑢 ∈ 𝑈) → 𝑈 = {𝑔 ∈ 𝐵 ∣ (𝑔 supp 0 ) ∈ 𝐴}) |
43 | 42 | eleq2d 2845 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑢 ∈ 𝑈) → (𝑣 ∈ 𝑈 ↔ 𝑣 ∈ {𝑔 ∈ 𝐵 ∣ (𝑔 supp 0 ) ∈ 𝐴})) |
44 | | oveq1 6931 |
. . . . . . . . . . . 12
⊢ (𝑔 = 𝑣 → (𝑔 supp 0 ) = (𝑣 supp 0 )) |
45 | 44 | eleq1d 2844 |
. . . . . . . . . . 11
⊢ (𝑔 = 𝑣 → ((𝑔 supp 0 ) ∈ 𝐴 ↔ (𝑣 supp 0 ) ∈ 𝐴)) |
46 | 45 | elrab 3572 |
. . . . . . . . . 10
⊢ (𝑣 ∈ {𝑔 ∈ 𝐵 ∣ (𝑔 supp 0 ) ∈ 𝐴} ↔ (𝑣 ∈ 𝐵 ∧ (𝑣 supp 0 ) ∈ 𝐴)) |
47 | 43, 46 | syl6bb 279 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑢 ∈ 𝑈) → (𝑣 ∈ 𝑈 ↔ (𝑣 ∈ 𝐵 ∧ (𝑣 supp 0 ) ∈ 𝐴))) |
48 | 47 | biimpa 470 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) → (𝑣 ∈ 𝐵 ∧ (𝑣 supp 0 ) ∈ 𝐴)) |
49 | 48 | simpld 490 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) → 𝑣 ∈ 𝐵) |
50 | 4, 9, 32, 33, 41, 49 | psraddcl 19784 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) → (𝑢(+g‘𝑆)𝑣) ∈ 𝐵) |
51 | | ovexd 6958 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) → ((𝑢(+g‘𝑆)𝑣) supp 0 ) ∈
V) |
52 | | sseq2 3846 |
. . . . . . . . . 10
⊢ (𝑥 = ((𝑢 supp 0 ) ∪ (𝑣 supp 0 )) → (𝑦 ⊆ 𝑥 ↔ 𝑦 ⊆ ((𝑢 supp 0 ) ∪ (𝑣 supp 0 )))) |
53 | 52 | imbi1d 333 |
. . . . . . . . 9
⊢ (𝑥 = ((𝑢 supp 0 ) ∪ (𝑣 supp 0 )) → ((𝑦 ⊆ 𝑥 → 𝑦 ∈ 𝐴) ↔ (𝑦 ⊆ ((𝑢 supp 0 ) ∪ (𝑣 supp 0 )) → 𝑦 ∈ 𝐴))) |
54 | 53 | albidv 1963 |
. . . . . . . 8
⊢ (𝑥 = ((𝑢 supp 0 ) ∪ (𝑣 supp 0 )) → (∀𝑦(𝑦 ⊆ 𝑥 → 𝑦 ∈ 𝐴) ↔ ∀𝑦(𝑦 ⊆ ((𝑢 supp 0 ) ∪ (𝑣 supp 0 )) → 𝑦 ∈ 𝐴))) |
55 | | mplsubglem.y |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ⊆ 𝑥)) → 𝑦 ∈ 𝐴) |
56 | 55 | expr 450 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝑦 ⊆ 𝑥 → 𝑦 ∈ 𝐴)) |
57 | 56 | alrimiv 1970 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ∀𝑦(𝑦 ⊆ 𝑥 → 𝑦 ∈ 𝐴)) |
58 | 57 | ralrimiva 3148 |
. . . . . . . . 9
⊢ (𝜑 → ∀𝑥 ∈ 𝐴 ∀𝑦(𝑦 ⊆ 𝑥 → 𝑦 ∈ 𝐴)) |
59 | 58 | ad2antrr 716 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) → ∀𝑥 ∈ 𝐴 ∀𝑦(𝑦 ⊆ 𝑥 → 𝑦 ∈ 𝐴)) |
60 | 39 | simprd 491 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑢 ∈ 𝑈) → (𝑢 supp 0 ) ∈ 𝐴) |
61 | 60 | adantr 474 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) → (𝑢 supp 0 ) ∈ 𝐴) |
62 | 48 | simprd 491 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) → (𝑣 supp 0 ) ∈ 𝐴) |
63 | | mplsubglem.a |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴)) → (𝑥 ∪ 𝑦) ∈ 𝐴) |
64 | 63 | ralrimivva 3153 |
. . . . . . . . . 10
⊢ (𝜑 → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ∪ 𝑦) ∈ 𝐴) |
65 | 64 | ad2antrr 716 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ∪ 𝑦) ∈ 𝐴) |
66 | | uneq1 3983 |
. . . . . . . . . . 11
⊢ (𝑥 = (𝑢 supp 0 ) → (𝑥 ∪ 𝑦) = ((𝑢 supp 0 ) ∪ 𝑦)) |
67 | 66 | eleq1d 2844 |
. . . . . . . . . 10
⊢ (𝑥 = (𝑢 supp 0 ) → ((𝑥 ∪ 𝑦) ∈ 𝐴 ↔ ((𝑢 supp 0 ) ∪ 𝑦) ∈ 𝐴)) |
68 | | uneq2 3984 |
. . . . . . . . . . 11
⊢ (𝑦 = (𝑣 supp 0 ) → ((𝑢 supp 0 ) ∪ 𝑦) = ((𝑢 supp 0 ) ∪ (𝑣 supp 0 ))) |
69 | 68 | eleq1d 2844 |
. . . . . . . . . 10
⊢ (𝑦 = (𝑣 supp 0 ) → (((𝑢 supp 0 ) ∪ 𝑦) ∈ 𝐴 ↔ ((𝑢 supp 0 ) ∪ (𝑣 supp 0 )) ∈ 𝐴)) |
70 | 67, 69 | rspc2va 3525 |
. . . . . . . . 9
⊢ ((((𝑢 supp 0 ) ∈ 𝐴 ∧ (𝑣 supp 0 ) ∈ 𝐴) ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ∪ 𝑦) ∈ 𝐴) → ((𝑢 supp 0 ) ∪ (𝑣 supp 0 )) ∈ 𝐴) |
71 | 61, 62, 65, 70 | syl21anc 828 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) → ((𝑢 supp 0 ) ∪ (𝑣 supp 0 )) ∈ 𝐴) |
72 | 54, 59, 71 | rspcdva 3517 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) → ∀𝑦(𝑦 ⊆ ((𝑢 supp 0 ) ∪ (𝑣 supp 0 )) → 𝑦 ∈ 𝐴)) |
73 | 4, 11, 7, 9, 50 | psrelbas 19780 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) → (𝑢(+g‘𝑆)𝑣):𝐷⟶(Base‘𝑅)) |
74 | | eqid 2778 |
. . . . . . . . . . . 12
⊢
(+g‘𝑅) = (+g‘𝑅) |
75 | 4, 9, 74, 32, 41, 49 | psradd 19783 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) → (𝑢(+g‘𝑆)𝑣) = (𝑢 ∘𝑓
(+g‘𝑅)𝑣)) |
76 | 75 | fveq1d 6450 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) → ((𝑢(+g‘𝑆)𝑣)‘𝑘) = ((𝑢 ∘𝑓
(+g‘𝑅)𝑣)‘𝑘)) |
77 | 76 | adantr 474 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) ∧ 𝑘 ∈ (𝐷 ∖ ((𝑢 supp 0 ) ∪ (𝑣 supp 0 )))) → ((𝑢(+g‘𝑆)𝑣)‘𝑘) = ((𝑢 ∘𝑓
(+g‘𝑅)𝑣)‘𝑘)) |
78 | | eldifi 3955 |
. . . . . . . . . 10
⊢ (𝑘 ∈ (𝐷 ∖ ((𝑢 supp 0 ) ∪ (𝑣 supp 0 ))) → 𝑘 ∈ 𝐷) |
79 | 4, 11, 7, 9, 40 | psrelbas 19780 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑢 ∈ 𝑈) → 𝑢:𝐷⟶(Base‘𝑅)) |
80 | 79 | adantr 474 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) → 𝑢:𝐷⟶(Base‘𝑅)) |
81 | 80 | ffnd 6294 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) → 𝑢 Fn 𝐷) |
82 | 4, 11, 7, 9, 49 | psrelbas 19780 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) → 𝑣:𝐷⟶(Base‘𝑅)) |
83 | 82 | ffnd 6294 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) → 𝑣 Fn 𝐷) |
84 | | ovex 6956 |
. . . . . . . . . . . . 13
⊢
(ℕ0 ↑𝑚 𝐼) ∈ V |
85 | 7, 84 | rabex2 5053 |
. . . . . . . . . . . 12
⊢ 𝐷 ∈ V |
86 | 85 | a1i 11 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) → 𝐷 ∈ V) |
87 | | inidm 4043 |
. . . . . . . . . . 11
⊢ (𝐷 ∩ 𝐷) = 𝐷 |
88 | | eqidd 2779 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) ∧ 𝑘 ∈ 𝐷) → (𝑢‘𝑘) = (𝑢‘𝑘)) |
89 | | eqidd 2779 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) ∧ 𝑘 ∈ 𝐷) → (𝑣‘𝑘) = (𝑣‘𝑘)) |
90 | 81, 83, 86, 86, 87, 88, 89 | ofval 7185 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) ∧ 𝑘 ∈ 𝐷) → ((𝑢 ∘𝑓
(+g‘𝑅)𝑣)‘𝑘) = ((𝑢‘𝑘)(+g‘𝑅)(𝑣‘𝑘))) |
91 | 78, 90 | sylan2 586 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) ∧ 𝑘 ∈ (𝐷 ∖ ((𝑢 supp 0 ) ∪ (𝑣 supp 0 )))) → ((𝑢 ∘𝑓
(+g‘𝑅)𝑣)‘𝑘) = ((𝑢‘𝑘)(+g‘𝑅)(𝑣‘𝑘))) |
92 | | ssun1 3999 |
. . . . . . . . . . . . . 14
⊢ (𝑢 supp 0 ) ⊆ ((𝑢 supp 0 ) ∪ (𝑣 supp 0 )) |
93 | | sscon 3967 |
. . . . . . . . . . . . . 14
⊢ ((𝑢 supp 0 ) ⊆ ((𝑢 supp 0 ) ∪ (𝑣 supp 0 )) → (𝐷 ∖ ((𝑢 supp 0 ) ∪ (𝑣 supp 0 ))) ⊆ (𝐷 ∖ (𝑢 supp 0 ))) |
94 | 92, 93 | ax-mp 5 |
. . . . . . . . . . . . 13
⊢ (𝐷 ∖ ((𝑢 supp 0 ) ∪ (𝑣 supp 0 ))) ⊆ (𝐷 ∖ (𝑢 supp 0 )) |
95 | 94 | sseli 3817 |
. . . . . . . . . . . 12
⊢ (𝑘 ∈ (𝐷 ∖ ((𝑢 supp 0 ) ∪ (𝑣 supp 0 ))) → 𝑘 ∈ (𝐷 ∖ (𝑢 supp 0 ))) |
96 | | ssidd 3843 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑢 ∈ 𝑈) → (𝑢 supp 0 ) ⊆ (𝑢 supp 0 )) |
97 | 85 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑢 ∈ 𝑈) → 𝐷 ∈ V) |
98 | 16 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑢 ∈ 𝑈) → 0 ∈ V) |
99 | 79, 96, 97, 98 | suppssr 7610 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑘 ∈ (𝐷 ∖ (𝑢 supp 0 ))) → (𝑢‘𝑘) = 0 ) |
100 | 99 | adantlr 705 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) ∧ 𝑘 ∈ (𝐷 ∖ (𝑢 supp 0 ))) → (𝑢‘𝑘) = 0 ) |
101 | 95, 100 | sylan2 586 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) ∧ 𝑘 ∈ (𝐷 ∖ ((𝑢 supp 0 ) ∪ (𝑣 supp 0 )))) → (𝑢‘𝑘) = 0 ) |
102 | | ssun2 4000 |
. . . . . . . . . . . . . 14
⊢ (𝑣 supp 0 ) ⊆ ((𝑢 supp 0 ) ∪ (𝑣 supp 0 )) |
103 | | sscon 3967 |
. . . . . . . . . . . . . 14
⊢ ((𝑣 supp 0 ) ⊆ ((𝑢 supp 0 ) ∪ (𝑣 supp 0 )) → (𝐷 ∖ ((𝑢 supp 0 ) ∪ (𝑣 supp 0 ))) ⊆ (𝐷 ∖ (𝑣 supp 0 ))) |
104 | 102, 103 | ax-mp 5 |
. . . . . . . . . . . . 13
⊢ (𝐷 ∖ ((𝑢 supp 0 ) ∪ (𝑣 supp 0 ))) ⊆ (𝐷 ∖ (𝑣 supp 0 )) |
105 | 104 | sseli 3817 |
. . . . . . . . . . . 12
⊢ (𝑘 ∈ (𝐷 ∖ ((𝑢 supp 0 ) ∪ (𝑣 supp 0 ))) → 𝑘 ∈ (𝐷 ∖ (𝑣 supp 0 ))) |
106 | | ssidd 3843 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) → (𝑣 supp 0 ) ⊆ (𝑣 supp 0 )) |
107 | 16 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) → 0 ∈ V) |
108 | 82, 106, 86, 107 | suppssr 7610 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) ∧ 𝑘 ∈ (𝐷 ∖ (𝑣 supp 0 ))) → (𝑣‘𝑘) = 0 ) |
109 | 105, 108 | sylan2 586 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) ∧ 𝑘 ∈ (𝐷 ∖ ((𝑢 supp 0 ) ∪ (𝑣 supp 0 )))) → (𝑣‘𝑘) = 0 ) |
110 | 101, 109 | oveq12d 6942 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) ∧ 𝑘 ∈ (𝐷 ∖ ((𝑢 supp 0 ) ∪ (𝑣 supp 0 )))) → ((𝑢‘𝑘)(+g‘𝑅)(𝑣‘𝑘)) = ( 0 (+g‘𝑅) 0 )) |
111 | 11, 74, 8 | grplid 17843 |
. . . . . . . . . . . . 13
⊢ ((𝑅 ∈ Grp ∧ 0 ∈
(Base‘𝑅)) → (
0
(+g‘𝑅)
0 ) =
0
) |
112 | 12, 111 | mpdan 677 |
. . . . . . . . . . . 12
⊢ (𝑅 ∈ Grp → ( 0
(+g‘𝑅)
0 ) =
0
) |
113 | 33, 112 | syl 17 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) → ( 0 (+g‘𝑅) 0 ) = 0 ) |
114 | 113 | adantr 474 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) ∧ 𝑘 ∈ (𝐷 ∖ ((𝑢 supp 0 ) ∪ (𝑣 supp 0 )))) → ( 0
(+g‘𝑅)
0 ) =
0
) |
115 | 110, 114 | eqtrd 2814 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) ∧ 𝑘 ∈ (𝐷 ∖ ((𝑢 supp 0 ) ∪ (𝑣 supp 0 )))) → ((𝑢‘𝑘)(+g‘𝑅)(𝑣‘𝑘)) = 0 ) |
116 | 77, 91, 115 | 3eqtrd 2818 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) ∧ 𝑘 ∈ (𝐷 ∖ ((𝑢 supp 0 ) ∪ (𝑣 supp 0 )))) → ((𝑢(+g‘𝑆)𝑣)‘𝑘) = 0 ) |
117 | 73, 116 | suppss 7609 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) → ((𝑢(+g‘𝑆)𝑣) supp 0 ) ⊆ ((𝑢 supp 0 ) ∪ (𝑣 supp 0 ))) |
118 | | sseq1 3845 |
. . . . . . . . 9
⊢ (𝑦 = ((𝑢(+g‘𝑆)𝑣) supp 0 ) → (𝑦 ⊆ ((𝑢 supp 0 ) ∪ (𝑣 supp 0 )) ↔ ((𝑢(+g‘𝑆)𝑣) supp 0 ) ⊆ ((𝑢 supp 0 ) ∪ (𝑣 supp 0 )))) |
119 | | eleq1 2847 |
. . . . . . . . 9
⊢ (𝑦 = ((𝑢(+g‘𝑆)𝑣) supp 0 ) → (𝑦 ∈ 𝐴 ↔ ((𝑢(+g‘𝑆)𝑣) supp 0 ) ∈ 𝐴)) |
120 | 118, 119 | imbi12d 336 |
. . . . . . . 8
⊢ (𝑦 = ((𝑢(+g‘𝑆)𝑣) supp 0 ) → ((𝑦 ⊆ ((𝑢 supp 0 ) ∪ (𝑣 supp 0 )) → 𝑦 ∈ 𝐴) ↔ (((𝑢(+g‘𝑆)𝑣) supp 0 ) ⊆ ((𝑢 supp 0 ) ∪ (𝑣 supp 0 )) → ((𝑢(+g‘𝑆)𝑣) supp 0 ) ∈ 𝐴))) |
121 | 120 | spcgv 3495 |
. . . . . . 7
⊢ (((𝑢(+g‘𝑆)𝑣) supp 0 ) ∈ V →
(∀𝑦(𝑦 ⊆ ((𝑢 supp 0 ) ∪ (𝑣 supp 0 )) → 𝑦 ∈ 𝐴) → (((𝑢(+g‘𝑆)𝑣) supp 0 ) ⊆ ((𝑢 supp 0 ) ∪ (𝑣 supp 0 )) → ((𝑢(+g‘𝑆)𝑣) supp 0 ) ∈ 𝐴))) |
122 | 51, 72, 117, 121 | syl3c 66 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) → ((𝑢(+g‘𝑆)𝑣) supp 0 ) ∈ 𝐴) |
123 | 1 | ad2antrr 716 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) → 𝑈 = {𝑔 ∈ 𝐵 ∣ (𝑔 supp 0 ) ∈ 𝐴}) |
124 | 123 | eleq2d 2845 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) → ((𝑢(+g‘𝑆)𝑣) ∈ 𝑈 ↔ (𝑢(+g‘𝑆)𝑣) ∈ {𝑔 ∈ 𝐵 ∣ (𝑔 supp 0 ) ∈ 𝐴})) |
125 | | oveq1 6931 |
. . . . . . . . 9
⊢ (𝑔 = (𝑢(+g‘𝑆)𝑣) → (𝑔 supp 0 ) = ((𝑢(+g‘𝑆)𝑣) supp 0 )) |
126 | 125 | eleq1d 2844 |
. . . . . . . 8
⊢ (𝑔 = (𝑢(+g‘𝑆)𝑣) → ((𝑔 supp 0 ) ∈ 𝐴 ↔ ((𝑢(+g‘𝑆)𝑣) supp 0 ) ∈ 𝐴)) |
127 | 126 | elrab 3572 |
. . . . . . 7
⊢ ((𝑢(+g‘𝑆)𝑣) ∈ {𝑔 ∈ 𝐵 ∣ (𝑔 supp 0 ) ∈ 𝐴} ↔ ((𝑢(+g‘𝑆)𝑣) ∈ 𝐵 ∧ ((𝑢(+g‘𝑆)𝑣) supp 0 ) ∈ 𝐴)) |
128 | 124, 127 | syl6bb 279 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) → ((𝑢(+g‘𝑆)𝑣) ∈ 𝑈 ↔ ((𝑢(+g‘𝑆)𝑣) ∈ 𝐵 ∧ ((𝑢(+g‘𝑆)𝑣) supp 0 ) ∈ 𝐴))) |
129 | 50, 122, 128 | mpbir2and 703 |
. . . . 5
⊢ (((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) → (𝑢(+g‘𝑆)𝑣) ∈ 𝑈) |
130 | 129 | ralrimiva 3148 |
. . . 4
⊢ ((𝜑 ∧ 𝑢 ∈ 𝑈) → ∀𝑣 ∈ 𝑈 (𝑢(+g‘𝑆)𝑣) ∈ 𝑈) |
131 | 4, 5, 6 | psrgrp 19799 |
. . . . . 6
⊢ (𝜑 → 𝑆 ∈ Grp) |
132 | | eqid 2778 |
. . . . . . 7
⊢
(invg‘𝑆) = (invg‘𝑆) |
133 | 9, 132 | grpinvcl 17858 |
. . . . . 6
⊢ ((𝑆 ∈ Grp ∧ 𝑢 ∈ 𝐵) → ((invg‘𝑆)‘𝑢) ∈ 𝐵) |
134 | 131, 40, 133 | syl2an2r 675 |
. . . . 5
⊢ ((𝜑 ∧ 𝑢 ∈ 𝑈) → ((invg‘𝑆)‘𝑢) ∈ 𝐵) |
135 | | ovexd 6958 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑢 ∈ 𝑈) → (((invg‘𝑆)‘𝑢) supp 0 ) ∈
V) |
136 | | sseq2 3846 |
. . . . . . . . 9
⊢ (𝑥 = (𝑢 supp 0 ) → (𝑦 ⊆ 𝑥 ↔ 𝑦 ⊆ (𝑢 supp 0 ))) |
137 | 136 | imbi1d 333 |
. . . . . . . 8
⊢ (𝑥 = (𝑢 supp 0 ) → ((𝑦 ⊆ 𝑥 → 𝑦 ∈ 𝐴) ↔ (𝑦 ⊆ (𝑢 supp 0 ) → 𝑦 ∈ 𝐴))) |
138 | 137 | albidv 1963 |
. . . . . . 7
⊢ (𝑥 = (𝑢 supp 0 ) → (∀𝑦(𝑦 ⊆ 𝑥 → 𝑦 ∈ 𝐴) ↔ ∀𝑦(𝑦 ⊆ (𝑢 supp 0 ) → 𝑦 ∈ 𝐴))) |
139 | 58 | adantr 474 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑢 ∈ 𝑈) → ∀𝑥 ∈ 𝐴 ∀𝑦(𝑦 ⊆ 𝑥 → 𝑦 ∈ 𝐴)) |
140 | 138, 139,
60 | rspcdva 3517 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑢 ∈ 𝑈) → ∀𝑦(𝑦 ⊆ (𝑢 supp 0 ) → 𝑦 ∈ 𝐴)) |
141 | 4, 11, 7, 9, 134 | psrelbas 19780 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑢 ∈ 𝑈) → ((invg‘𝑆)‘𝑢):𝐷⟶(Base‘𝑅)) |
142 | 5 | adantr 474 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑢 ∈ 𝑈) → 𝐼 ∈ 𝑊) |
143 | 6 | adantr 474 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑢 ∈ 𝑈) → 𝑅 ∈ Grp) |
144 | | eqid 2778 |
. . . . . . . . . . 11
⊢
(invg‘𝑅) = (invg‘𝑅) |
145 | 4, 142, 143, 7, 144, 9, 132, 40 | psrneg 19801 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑢 ∈ 𝑈) → ((invg‘𝑆)‘𝑢) = ((invg‘𝑅) ∘ 𝑢)) |
146 | 145 | adantr 474 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑘 ∈ (𝐷 ∖ (𝑢 supp 0 ))) →
((invg‘𝑆)‘𝑢) = ((invg‘𝑅) ∘ 𝑢)) |
147 | 146 | fveq1d 6450 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑘 ∈ (𝐷 ∖ (𝑢 supp 0 ))) →
(((invg‘𝑆)‘𝑢)‘𝑘) = (((invg‘𝑅) ∘ 𝑢)‘𝑘)) |
148 | | eldifi 3955 |
. . . . . . . . 9
⊢ (𝑘 ∈ (𝐷 ∖ (𝑢 supp 0 )) → 𝑘 ∈ 𝐷) |
149 | | fvco3 6537 |
. . . . . . . . 9
⊢ ((𝑢:𝐷⟶(Base‘𝑅) ∧ 𝑘 ∈ 𝐷) → (((invg‘𝑅) ∘ 𝑢)‘𝑘) = ((invg‘𝑅)‘(𝑢‘𝑘))) |
150 | 79, 148, 149 | syl2an 589 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑘 ∈ (𝐷 ∖ (𝑢 supp 0 ))) →
(((invg‘𝑅)
∘ 𝑢)‘𝑘) =
((invg‘𝑅)‘(𝑢‘𝑘))) |
151 | 99 | fveq2d 6452 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑘 ∈ (𝐷 ∖ (𝑢 supp 0 ))) →
((invg‘𝑅)‘(𝑢‘𝑘)) = ((invg‘𝑅)‘ 0 )) |
152 | 8, 144 | grpinvid 17867 |
. . . . . . . . . . 11
⊢ (𝑅 ∈ Grp →
((invg‘𝑅)‘ 0 ) = 0 ) |
153 | 143, 152 | syl 17 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑢 ∈ 𝑈) → ((invg‘𝑅)‘ 0 ) = 0 ) |
154 | 153 | adantr 474 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑘 ∈ (𝐷 ∖ (𝑢 supp 0 ))) →
((invg‘𝑅)‘ 0 ) = 0 ) |
155 | 151, 154 | eqtrd 2814 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑘 ∈ (𝐷 ∖ (𝑢 supp 0 ))) →
((invg‘𝑅)‘(𝑢‘𝑘)) = 0 ) |
156 | 147, 150,
155 | 3eqtrd 2818 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑘 ∈ (𝐷 ∖ (𝑢 supp 0 ))) →
(((invg‘𝑆)‘𝑢)‘𝑘) = 0 ) |
157 | 141, 156 | suppss 7609 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑢 ∈ 𝑈) → (((invg‘𝑆)‘𝑢) supp 0 ) ⊆ (𝑢 supp 0 )) |
158 | | sseq1 3845 |
. . . . . . . 8
⊢ (𝑦 =
(((invg‘𝑆)‘𝑢) supp 0 ) → (𝑦 ⊆ (𝑢 supp 0 ) ↔
(((invg‘𝑆)‘𝑢) supp 0 ) ⊆ (𝑢 supp 0 ))) |
159 | | eleq1 2847 |
. . . . . . . 8
⊢ (𝑦 =
(((invg‘𝑆)‘𝑢) supp 0 ) → (𝑦 ∈ 𝐴 ↔ (((invg‘𝑆)‘𝑢) supp 0 ) ∈ 𝐴)) |
160 | 158, 159 | imbi12d 336 |
. . . . . . 7
⊢ (𝑦 =
(((invg‘𝑆)‘𝑢) supp 0 ) → ((𝑦 ⊆ (𝑢 supp 0 ) → 𝑦 ∈ 𝐴) ↔ ((((invg‘𝑆)‘𝑢) supp 0 ) ⊆ (𝑢 supp 0 ) →
(((invg‘𝑆)‘𝑢) supp 0 ) ∈ 𝐴))) |
161 | 160 | spcgv 3495 |
. . . . . 6
⊢
((((invg‘𝑆)‘𝑢) supp 0 ) ∈ V →
(∀𝑦(𝑦 ⊆ (𝑢 supp 0 ) → 𝑦 ∈ 𝐴) → ((((invg‘𝑆)‘𝑢) supp 0 ) ⊆ (𝑢 supp 0 ) →
(((invg‘𝑆)‘𝑢) supp 0 ) ∈ 𝐴))) |
162 | 135, 140,
157, 161 | syl3c 66 |
. . . . 5
⊢ ((𝜑 ∧ 𝑢 ∈ 𝑈) → (((invg‘𝑆)‘𝑢) supp 0 ) ∈ 𝐴) |
163 | 42 | eleq2d 2845 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑢 ∈ 𝑈) → (((invg‘𝑆)‘𝑢) ∈ 𝑈 ↔ ((invg‘𝑆)‘𝑢) ∈ {𝑔 ∈ 𝐵 ∣ (𝑔 supp 0 ) ∈ 𝐴})) |
164 | | oveq1 6931 |
. . . . . . . 8
⊢ (𝑔 = ((invg‘𝑆)‘𝑢) → (𝑔 supp 0 ) =
(((invg‘𝑆)‘𝑢) supp 0 )) |
165 | 164 | eleq1d 2844 |
. . . . . . 7
⊢ (𝑔 = ((invg‘𝑆)‘𝑢) → ((𝑔 supp 0 ) ∈ 𝐴 ↔ (((invg‘𝑆)‘𝑢) supp 0 ) ∈ 𝐴)) |
166 | 165 | elrab 3572 |
. . . . . 6
⊢
(((invg‘𝑆)‘𝑢) ∈ {𝑔 ∈ 𝐵 ∣ (𝑔 supp 0 ) ∈ 𝐴} ↔ (((invg‘𝑆)‘𝑢) ∈ 𝐵 ∧ (((invg‘𝑆)‘𝑢) supp 0 ) ∈ 𝐴)) |
167 | 163, 166 | syl6bb 279 |
. . . . 5
⊢ ((𝜑 ∧ 𝑢 ∈ 𝑈) → (((invg‘𝑆)‘𝑢) ∈ 𝑈 ↔ (((invg‘𝑆)‘𝑢) ∈ 𝐵 ∧ (((invg‘𝑆)‘𝑢) supp 0 ) ∈ 𝐴))) |
168 | 134, 162,
167 | mpbir2and 703 |
. . . 4
⊢ ((𝜑 ∧ 𝑢 ∈ 𝑈) → ((invg‘𝑆)‘𝑢) ∈ 𝑈) |
169 | 130, 168 | jca 507 |
. . 3
⊢ ((𝜑 ∧ 𝑢 ∈ 𝑈) → (∀𝑣 ∈ 𝑈 (𝑢(+g‘𝑆)𝑣) ∈ 𝑈 ∧ ((invg‘𝑆)‘𝑢) ∈ 𝑈)) |
170 | 169 | ralrimiva 3148 |
. 2
⊢ (𝜑 → ∀𝑢 ∈ 𝑈 (∀𝑣 ∈ 𝑈 (𝑢(+g‘𝑆)𝑣) ∈ 𝑈 ∧ ((invg‘𝑆)‘𝑢) ∈ 𝑈)) |
171 | 9, 32, 132 | issubg2 17997 |
. . 3
⊢ (𝑆 ∈ Grp → (𝑈 ∈ (SubGrp‘𝑆) ↔ (𝑈 ⊆ 𝐵 ∧ 𝑈 ≠ ∅ ∧ ∀𝑢 ∈ 𝑈 (∀𝑣 ∈ 𝑈 (𝑢(+g‘𝑆)𝑣) ∈ 𝑈 ∧ ((invg‘𝑆)‘𝑢) ∈ 𝑈)))) |
172 | 131, 171 | syl 17 |
. 2
⊢ (𝜑 → (𝑈 ∈ (SubGrp‘𝑆) ↔ (𝑈 ⊆ 𝐵 ∧ 𝑈 ≠ ∅ ∧ ∀𝑢 ∈ 𝑈 (∀𝑣 ∈ 𝑈 (𝑢(+g‘𝑆)𝑣) ∈ 𝑈 ∧ ((invg‘𝑆)‘𝑢) ∈ 𝑈)))) |
173 | 3, 31, 170, 172 | mpbir3and 1399 |
1
⊢ (𝜑 → 𝑈 ∈ (SubGrp‘𝑆)) |