Step | Hyp | Ref
| Expression |
1 | | mplsubglem.u |
. . 3
⊢ (𝜑 → 𝑈 = {𝑔 ∈ 𝐵 ∣ (𝑔 supp 0 ) ∈ 𝐴}) |
2 | | ssrab2 3650 |
. . 3
⊢ {𝑔 ∈ 𝐵 ∣ (𝑔 supp 0 ) ∈ 𝐴} ⊆ 𝐵 |
3 | 1, 2 | syl6eqss 3618 |
. 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 19215 |
. . . 4
⊢ (𝜑 → (𝐷 × { 0 }) ∈ 𝐵) |
11 | | eqid 2610 |
. . . . . . . . 9
⊢
(Base‘𝑅) =
(Base‘𝑅) |
12 | 11, 8 | grpidcl 17273 |
. . . . . . . 8
⊢ (𝑅 ∈ Grp → 0 ∈
(Base‘𝑅)) |
13 | | fconst6g 6007 |
. . . . . . . 8
⊢ ( 0 ∈
(Base‘𝑅) →
(𝐷 × { 0 }):𝐷⟶(Base‘𝑅)) |
14 | 6, 12, 13 | 3syl 18 |
. . . . . . 7
⊢ (𝜑 → (𝐷 × { 0 }):𝐷⟶(Base‘𝑅)) |
15 | | eldifi 3694 |
. . . . . . . . 9
⊢ (𝑢 ∈ (𝐷 ∖ ∅) → 𝑢 ∈ 𝐷) |
16 | | fvex 6113 |
. . . . . . . . . . 11
⊢
(0g‘𝑅) ∈ V |
17 | 8, 16 | eqeltri 2684 |
. . . . . . . . . 10
⊢ 0 ∈
V |
18 | 17 | fvconst2 6374 |
. . . . . . . . 9
⊢ (𝑢 ∈ 𝐷 → ((𝐷 × { 0 })‘𝑢) = 0 ) |
19 | 15, 18 | syl 17 |
. . . . . . . 8
⊢ (𝑢 ∈ (𝐷 ∖ ∅) → ((𝐷 × { 0 })‘𝑢) = 0 ) |
20 | 19 | adantl 481 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑢 ∈ (𝐷 ∖ ∅)) → ((𝐷 × { 0 })‘𝑢) = 0 ) |
21 | 14, 20 | suppss 7212 |
. . . . . 6
⊢ (𝜑 → ((𝐷 × { 0 }) supp 0 ) ⊆
∅) |
22 | | ss0 3926 |
. . . . . 6
⊢ (((𝐷 × { 0 }) supp 0 ) ⊆ ∅ →
((𝐷 × { 0 }) supp 0 ) =
∅) |
23 | 21, 22 | syl 17 |
. . . . 5
⊢ (𝜑 → ((𝐷 × { 0 }) supp 0 ) =
∅) |
24 | | mplsubglem.0 |
. . . . 5
⊢ (𝜑 → ∅ ∈ 𝐴) |
25 | 23, 24 | eqeltrd 2688 |
. . . 4
⊢ (𝜑 → ((𝐷 × { 0 }) supp 0 ) ∈ 𝐴) |
26 | 1 | eleq2d 2673 |
. . . . 5
⊢ (𝜑 → ((𝐷 × { 0 }) ∈ 𝑈 ↔ (𝐷 × { 0 }) ∈ {𝑔 ∈ 𝐵 ∣ (𝑔 supp 0 ) ∈ 𝐴})) |
27 | | oveq1 6556 |
. . . . . . 7
⊢ (𝑔 = (𝐷 × { 0 }) → (𝑔 supp 0 ) = ((𝐷 × { 0 }) supp 0 )) |
28 | 27 | eleq1d 2672 |
. . . . . 6
⊢ (𝑔 = (𝐷 × { 0 }) → ((𝑔 supp 0 ) ∈ 𝐴 ↔ ((𝐷 × { 0 }) supp 0 ) ∈ 𝐴)) |
29 | 28 | elrab 3331 |
. . . . 5
⊢ ((𝐷 × { 0 }) ∈ {𝑔 ∈ 𝐵 ∣ (𝑔 supp 0 ) ∈ 𝐴} ↔ ((𝐷 × { 0 }) ∈ 𝐵 ∧ ((𝐷 × { 0 }) supp 0 ) ∈ 𝐴)) |
30 | 26, 29 | syl6bb 275 |
. . . 4
⊢ (𝜑 → ((𝐷 × { 0 }) ∈ 𝑈 ↔ ((𝐷 × { 0 }) ∈ 𝐵 ∧ ((𝐷 × { 0 }) supp 0 ) ∈ 𝐴))) |
31 | 10, 25, 30 | mpbir2and 959 |
. . 3
⊢ (𝜑 → (𝐷 × { 0 }) ∈ 𝑈) |
32 | | ne0i 3880 |
. . 3
⊢ ((𝐷 × { 0 }) ∈ 𝑈 → 𝑈 ≠ ∅) |
33 | 31, 32 | syl 17 |
. 2
⊢ (𝜑 → 𝑈 ≠ ∅) |
34 | | eqid 2610 |
. . . . . . 7
⊢
(+g‘𝑆) = (+g‘𝑆) |
35 | 6 | ad2antrr 758 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) → 𝑅 ∈ Grp) |
36 | 1 | eleq2d 2673 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑢 ∈ 𝑈 ↔ 𝑢 ∈ {𝑔 ∈ 𝐵 ∣ (𝑔 supp 0 ) ∈ 𝐴})) |
37 | | oveq1 6556 |
. . . . . . . . . . . . 13
⊢ (𝑔 = 𝑢 → (𝑔 supp 0 ) = (𝑢 supp 0 )) |
38 | 37 | eleq1d 2672 |
. . . . . . . . . . . 12
⊢ (𝑔 = 𝑢 → ((𝑔 supp 0 ) ∈ 𝐴 ↔ (𝑢 supp 0 ) ∈ 𝐴)) |
39 | 38 | elrab 3331 |
. . . . . . . . . . 11
⊢ (𝑢 ∈ {𝑔 ∈ 𝐵 ∣ (𝑔 supp 0 ) ∈ 𝐴} ↔ (𝑢 ∈ 𝐵 ∧ (𝑢 supp 0 ) ∈ 𝐴)) |
40 | 36, 39 | syl6bb 275 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑢 ∈ 𝑈 ↔ (𝑢 ∈ 𝐵 ∧ (𝑢 supp 0 ) ∈ 𝐴))) |
41 | 40 | biimpa 500 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑢 ∈ 𝑈) → (𝑢 ∈ 𝐵 ∧ (𝑢 supp 0 ) ∈ 𝐴)) |
42 | 41 | simpld 474 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑢 ∈ 𝑈) → 𝑢 ∈ 𝐵) |
43 | 42 | adantr 480 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) → 𝑢 ∈ 𝐵) |
44 | 1 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑢 ∈ 𝑈) → 𝑈 = {𝑔 ∈ 𝐵 ∣ (𝑔 supp 0 ) ∈ 𝐴}) |
45 | 44 | eleq2d 2673 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑢 ∈ 𝑈) → (𝑣 ∈ 𝑈 ↔ 𝑣 ∈ {𝑔 ∈ 𝐵 ∣ (𝑔 supp 0 ) ∈ 𝐴})) |
46 | | oveq1 6556 |
. . . . . . . . . . . 12
⊢ (𝑔 = 𝑣 → (𝑔 supp 0 ) = (𝑣 supp 0 )) |
47 | 46 | eleq1d 2672 |
. . . . . . . . . . 11
⊢ (𝑔 = 𝑣 → ((𝑔 supp 0 ) ∈ 𝐴 ↔ (𝑣 supp 0 ) ∈ 𝐴)) |
48 | 47 | elrab 3331 |
. . . . . . . . . 10
⊢ (𝑣 ∈ {𝑔 ∈ 𝐵 ∣ (𝑔 supp 0 ) ∈ 𝐴} ↔ (𝑣 ∈ 𝐵 ∧ (𝑣 supp 0 ) ∈ 𝐴)) |
49 | 45, 48 | syl6bb 275 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑢 ∈ 𝑈) → (𝑣 ∈ 𝑈 ↔ (𝑣 ∈ 𝐵 ∧ (𝑣 supp 0 ) ∈ 𝐴))) |
50 | 49 | biimpa 500 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) → (𝑣 ∈ 𝐵 ∧ (𝑣 supp 0 ) ∈ 𝐴)) |
51 | 50 | simpld 474 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) → 𝑣 ∈ 𝐵) |
52 | 4, 9, 34, 35, 43, 51 | psraddcl 19204 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) → (𝑢(+g‘𝑆)𝑣) ∈ 𝐵) |
53 | | ovex 6577 |
. . . . . . . 8
⊢ ((𝑢(+g‘𝑆)𝑣) supp 0 ) ∈
V |
54 | 53 | a1i 11 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) → ((𝑢(+g‘𝑆)𝑣) supp 0 ) ∈
V) |
55 | 41 | simprd 478 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑢 ∈ 𝑈) → (𝑢 supp 0 ) ∈ 𝐴) |
56 | 55 | adantr 480 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) → (𝑢 supp 0 ) ∈ 𝐴) |
57 | 50 | simprd 478 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) → (𝑣 supp 0 ) ∈ 𝐴) |
58 | | mplsubglem.a |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴)) → (𝑥 ∪ 𝑦) ∈ 𝐴) |
59 | 58 | ralrimivva 2954 |
. . . . . . . . . 10
⊢ (𝜑 → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ∪ 𝑦) ∈ 𝐴) |
60 | 59 | ad2antrr 758 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ∪ 𝑦) ∈ 𝐴) |
61 | | uneq1 3722 |
. . . . . . . . . . 11
⊢ (𝑥 = (𝑢 supp 0 ) → (𝑥 ∪ 𝑦) = ((𝑢 supp 0 ) ∪ 𝑦)) |
62 | 61 | eleq1d 2672 |
. . . . . . . . . 10
⊢ (𝑥 = (𝑢 supp 0 ) → ((𝑥 ∪ 𝑦) ∈ 𝐴 ↔ ((𝑢 supp 0 ) ∪ 𝑦) ∈ 𝐴)) |
63 | | uneq2 3723 |
. . . . . . . . . . 11
⊢ (𝑦 = (𝑣 supp 0 ) → ((𝑢 supp 0 ) ∪ 𝑦) = ((𝑢 supp 0 ) ∪ (𝑣 supp 0 ))) |
64 | 63 | eleq1d 2672 |
. . . . . . . . . 10
⊢ (𝑦 = (𝑣 supp 0 ) → (((𝑢 supp 0 ) ∪ 𝑦) ∈ 𝐴 ↔ ((𝑢 supp 0 ) ∪ (𝑣 supp 0 )) ∈ 𝐴)) |
65 | 62, 64 | rspc2va 3294 |
. . . . . . . . 9
⊢ ((((𝑢 supp 0 ) ∈ 𝐴 ∧ (𝑣 supp 0 ) ∈ 𝐴) ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ∪ 𝑦) ∈ 𝐴) → ((𝑢 supp 0 ) ∪ (𝑣 supp 0 )) ∈ 𝐴) |
66 | 56, 57, 60, 65 | syl21anc 1317 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) → ((𝑢 supp 0 ) ∪ (𝑣 supp 0 )) ∈ 𝐴) |
67 | | mplsubglem.y |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ⊆ 𝑥)) → 𝑦 ∈ 𝐴) |
68 | 67 | expr 641 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝑦 ⊆ 𝑥 → 𝑦 ∈ 𝐴)) |
69 | 68 | alrimiv 1842 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ∀𝑦(𝑦 ⊆ 𝑥 → 𝑦 ∈ 𝐴)) |
70 | 69 | ralrimiva 2949 |
. . . . . . . . 9
⊢ (𝜑 → ∀𝑥 ∈ 𝐴 ∀𝑦(𝑦 ⊆ 𝑥 → 𝑦 ∈ 𝐴)) |
71 | 70 | ad2antrr 758 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) → ∀𝑥 ∈ 𝐴 ∀𝑦(𝑦 ⊆ 𝑥 → 𝑦 ∈ 𝐴)) |
72 | | sseq2 3590 |
. . . . . . . . . . 11
⊢ (𝑥 = ((𝑢 supp 0 ) ∪ (𝑣 supp 0 )) → (𝑦 ⊆ 𝑥 ↔ 𝑦 ⊆ ((𝑢 supp 0 ) ∪ (𝑣 supp 0 )))) |
73 | 72 | imbi1d 330 |
. . . . . . . . . 10
⊢ (𝑥 = ((𝑢 supp 0 ) ∪ (𝑣 supp 0 )) → ((𝑦 ⊆ 𝑥 → 𝑦 ∈ 𝐴) ↔ (𝑦 ⊆ ((𝑢 supp 0 ) ∪ (𝑣 supp 0 )) → 𝑦 ∈ 𝐴))) |
74 | 73 | albidv 1836 |
. . . . . . . . 9
⊢ (𝑥 = ((𝑢 supp 0 ) ∪ (𝑣 supp 0 )) → (∀𝑦(𝑦 ⊆ 𝑥 → 𝑦 ∈ 𝐴) ↔ ∀𝑦(𝑦 ⊆ ((𝑢 supp 0 ) ∪ (𝑣 supp 0 )) → 𝑦 ∈ 𝐴))) |
75 | 74 | rspcv 3278 |
. . . . . . . 8
⊢ (((𝑢 supp 0 ) ∪ (𝑣 supp 0 )) ∈ 𝐴 → (∀𝑥 ∈ 𝐴 ∀𝑦(𝑦 ⊆ 𝑥 → 𝑦 ∈ 𝐴) → ∀𝑦(𝑦 ⊆ ((𝑢 supp 0 ) ∪ (𝑣 supp 0 )) → 𝑦 ∈ 𝐴))) |
76 | 66, 71, 75 | sylc 63 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) → ∀𝑦(𝑦 ⊆ ((𝑢 supp 0 ) ∪ (𝑣 supp 0 )) → 𝑦 ∈ 𝐴)) |
77 | 4, 11, 7, 9, 52 | psrelbas 19200 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) → (𝑢(+g‘𝑆)𝑣):𝐷⟶(Base‘𝑅)) |
78 | | eqid 2610 |
. . . . . . . . . . . 12
⊢
(+g‘𝑅) = (+g‘𝑅) |
79 | 4, 9, 78, 34, 43, 51 | psradd 19203 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) → (𝑢(+g‘𝑆)𝑣) = (𝑢 ∘𝑓
(+g‘𝑅)𝑣)) |
80 | 79 | fveq1d 6105 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) → ((𝑢(+g‘𝑆)𝑣)‘𝑘) = ((𝑢 ∘𝑓
(+g‘𝑅)𝑣)‘𝑘)) |
81 | 80 | adantr 480 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) ∧ 𝑘 ∈ (𝐷 ∖ ((𝑢 supp 0 ) ∪ (𝑣 supp 0 )))) → ((𝑢(+g‘𝑆)𝑣)‘𝑘) = ((𝑢 ∘𝑓
(+g‘𝑅)𝑣)‘𝑘)) |
82 | | eldifi 3694 |
. . . . . . . . . 10
⊢ (𝑘 ∈ (𝐷 ∖ ((𝑢 supp 0 ) ∪ (𝑣 supp 0 ))) → 𝑘 ∈ 𝐷) |
83 | 4, 11, 7, 9, 42 | psrelbas 19200 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑢 ∈ 𝑈) → 𝑢:𝐷⟶(Base‘𝑅)) |
84 | 83 | adantr 480 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) → 𝑢:𝐷⟶(Base‘𝑅)) |
85 | 84 | ffnd 5959 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) → 𝑢 Fn 𝐷) |
86 | 4, 11, 7, 9, 51 | psrelbas 19200 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) → 𝑣:𝐷⟶(Base‘𝑅)) |
87 | 86 | ffnd 5959 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) → 𝑣 Fn 𝐷) |
88 | | ovex 6577 |
. . . . . . . . . . . . 13
⊢
(ℕ0 ↑𝑚 𝐼) ∈ V |
89 | 7, 88 | rabex2 4742 |
. . . . . . . . . . . 12
⊢ 𝐷 ∈ V |
90 | 89 | a1i 11 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) → 𝐷 ∈ V) |
91 | | inidm 3784 |
. . . . . . . . . . 11
⊢ (𝐷 ∩ 𝐷) = 𝐷 |
92 | | eqidd 2611 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) ∧ 𝑘 ∈ 𝐷) → (𝑢‘𝑘) = (𝑢‘𝑘)) |
93 | | eqidd 2611 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) ∧ 𝑘 ∈ 𝐷) → (𝑣‘𝑘) = (𝑣‘𝑘)) |
94 | 85, 87, 90, 90, 91, 92, 93 | ofval 6804 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) ∧ 𝑘 ∈ 𝐷) → ((𝑢 ∘𝑓
(+g‘𝑅)𝑣)‘𝑘) = ((𝑢‘𝑘)(+g‘𝑅)(𝑣‘𝑘))) |
95 | 82, 94 | sylan2 490 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) ∧ 𝑘 ∈ (𝐷 ∖ ((𝑢 supp 0 ) ∪ (𝑣 supp 0 )))) → ((𝑢 ∘𝑓
(+g‘𝑅)𝑣)‘𝑘) = ((𝑢‘𝑘)(+g‘𝑅)(𝑣‘𝑘))) |
96 | | ssun1 3738 |
. . . . . . . . . . . . . 14
⊢ (𝑢 supp 0 ) ⊆ ((𝑢 supp 0 ) ∪ (𝑣 supp 0 )) |
97 | | sscon 3706 |
. . . . . . . . . . . . . 14
⊢ ((𝑢 supp 0 ) ⊆ ((𝑢 supp 0 ) ∪ (𝑣 supp 0 )) → (𝐷 ∖ ((𝑢 supp 0 ) ∪ (𝑣 supp 0 ))) ⊆ (𝐷 ∖ (𝑢 supp 0 ))) |
98 | 96, 97 | ax-mp 5 |
. . . . . . . . . . . . 13
⊢ (𝐷 ∖ ((𝑢 supp 0 ) ∪ (𝑣 supp 0 ))) ⊆ (𝐷 ∖ (𝑢 supp 0 )) |
99 | 98 | sseli 3564 |
. . . . . . . . . . . 12
⊢ (𝑘 ∈ (𝐷 ∖ ((𝑢 supp 0 ) ∪ (𝑣 supp 0 ))) → 𝑘 ∈ (𝐷 ∖ (𝑢 supp 0 ))) |
100 | | ssid 3587 |
. . . . . . . . . . . . . . 15
⊢ (𝑢 supp 0 ) ⊆ (𝑢 supp 0 ) |
101 | 100 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑢 ∈ 𝑈) → (𝑢 supp 0 ) ⊆ (𝑢 supp 0 )) |
102 | 89 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑢 ∈ 𝑈) → 𝐷 ∈ V) |
103 | 17 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑢 ∈ 𝑈) → 0 ∈ V) |
104 | 83, 101, 102, 103 | suppssr 7213 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑘 ∈ (𝐷 ∖ (𝑢 supp 0 ))) → (𝑢‘𝑘) = 0 ) |
105 | 104 | adantlr 747 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) ∧ 𝑘 ∈ (𝐷 ∖ (𝑢 supp 0 ))) → (𝑢‘𝑘) = 0 ) |
106 | 99, 105 | sylan2 490 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) ∧ 𝑘 ∈ (𝐷 ∖ ((𝑢 supp 0 ) ∪ (𝑣 supp 0 )))) → (𝑢‘𝑘) = 0 ) |
107 | | ssun2 3739 |
. . . . . . . . . . . . . 14
⊢ (𝑣 supp 0 ) ⊆ ((𝑢 supp 0 ) ∪ (𝑣 supp 0 )) |
108 | | sscon 3706 |
. . . . . . . . . . . . . 14
⊢ ((𝑣 supp 0 ) ⊆ ((𝑢 supp 0 ) ∪ (𝑣 supp 0 )) → (𝐷 ∖ ((𝑢 supp 0 ) ∪ (𝑣 supp 0 ))) ⊆ (𝐷 ∖ (𝑣 supp 0 ))) |
109 | 107, 108 | ax-mp 5 |
. . . . . . . . . . . . 13
⊢ (𝐷 ∖ ((𝑢 supp 0 ) ∪ (𝑣 supp 0 ))) ⊆ (𝐷 ∖ (𝑣 supp 0 )) |
110 | 109 | sseli 3564 |
. . . . . . . . . . . 12
⊢ (𝑘 ∈ (𝐷 ∖ ((𝑢 supp 0 ) ∪ (𝑣 supp 0 ))) → 𝑘 ∈ (𝐷 ∖ (𝑣 supp 0 ))) |
111 | | ssid 3587 |
. . . . . . . . . . . . . 14
⊢ (𝑣 supp 0 ) ⊆ (𝑣 supp 0 ) |
112 | 111 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) → (𝑣 supp 0 ) ⊆ (𝑣 supp 0 )) |
113 | 17 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) → 0 ∈ V) |
114 | 86, 112, 90, 113 | suppssr 7213 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) ∧ 𝑘 ∈ (𝐷 ∖ (𝑣 supp 0 ))) → (𝑣‘𝑘) = 0 ) |
115 | 110, 114 | sylan2 490 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) ∧ 𝑘 ∈ (𝐷 ∖ ((𝑢 supp 0 ) ∪ (𝑣 supp 0 )))) → (𝑣‘𝑘) = 0 ) |
116 | 106, 115 | oveq12d 6567 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) ∧ 𝑘 ∈ (𝐷 ∖ ((𝑢 supp 0 ) ∪ (𝑣 supp 0 )))) → ((𝑢‘𝑘)(+g‘𝑅)(𝑣‘𝑘)) = ( 0 (+g‘𝑅) 0 )) |
117 | 11, 78, 8 | grplid 17275 |
. . . . . . . . . . . . 13
⊢ ((𝑅 ∈ Grp ∧ 0 ∈
(Base‘𝑅)) → (
0
(+g‘𝑅)
0 ) =
0
) |
118 | 12, 117 | mpdan 699 |
. . . . . . . . . . . 12
⊢ (𝑅 ∈ Grp → ( 0
(+g‘𝑅)
0 ) =
0
) |
119 | 35, 118 | syl 17 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) → ( 0 (+g‘𝑅) 0 ) = 0 ) |
120 | 119 | adantr 480 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) ∧ 𝑘 ∈ (𝐷 ∖ ((𝑢 supp 0 ) ∪ (𝑣 supp 0 )))) → ( 0
(+g‘𝑅)
0 ) =
0
) |
121 | 116, 120 | eqtrd 2644 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) ∧ 𝑘 ∈ (𝐷 ∖ ((𝑢 supp 0 ) ∪ (𝑣 supp 0 )))) → ((𝑢‘𝑘)(+g‘𝑅)(𝑣‘𝑘)) = 0 ) |
122 | 81, 95, 121 | 3eqtrd 2648 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) ∧ 𝑘 ∈ (𝐷 ∖ ((𝑢 supp 0 ) ∪ (𝑣 supp 0 )))) → ((𝑢(+g‘𝑆)𝑣)‘𝑘) = 0 ) |
123 | 77, 122 | suppss 7212 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) → ((𝑢(+g‘𝑆)𝑣) supp 0 ) ⊆ ((𝑢 supp 0 ) ∪ (𝑣 supp 0 ))) |
124 | | sseq1 3589 |
. . . . . . . . 9
⊢ (𝑦 = ((𝑢(+g‘𝑆)𝑣) supp 0 ) → (𝑦 ⊆ ((𝑢 supp 0 ) ∪ (𝑣 supp 0 )) ↔ ((𝑢(+g‘𝑆)𝑣) supp 0 ) ⊆ ((𝑢 supp 0 ) ∪ (𝑣 supp 0 )))) |
125 | | eleq1 2676 |
. . . . . . . . 9
⊢ (𝑦 = ((𝑢(+g‘𝑆)𝑣) supp 0 ) → (𝑦 ∈ 𝐴 ↔ ((𝑢(+g‘𝑆)𝑣) supp 0 ) ∈ 𝐴)) |
126 | 124, 125 | imbi12d 333 |
. . . . . . . 8
⊢ (𝑦 = ((𝑢(+g‘𝑆)𝑣) supp 0 ) → ((𝑦 ⊆ ((𝑢 supp 0 ) ∪ (𝑣 supp 0 )) → 𝑦 ∈ 𝐴) ↔ (((𝑢(+g‘𝑆)𝑣) supp 0 ) ⊆ ((𝑢 supp 0 ) ∪ (𝑣 supp 0 )) → ((𝑢(+g‘𝑆)𝑣) supp 0 ) ∈ 𝐴))) |
127 | 126 | spcgv 3266 |
. . . . . . 7
⊢ (((𝑢(+g‘𝑆)𝑣) supp 0 ) ∈ V →
(∀𝑦(𝑦 ⊆ ((𝑢 supp 0 ) ∪ (𝑣 supp 0 )) → 𝑦 ∈ 𝐴) → (((𝑢(+g‘𝑆)𝑣) supp 0 ) ⊆ ((𝑢 supp 0 ) ∪ (𝑣 supp 0 )) → ((𝑢(+g‘𝑆)𝑣) supp 0 ) ∈ 𝐴))) |
128 | 54, 76, 123, 127 | syl3c 64 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) → ((𝑢(+g‘𝑆)𝑣) supp 0 ) ∈ 𝐴) |
129 | 1 | ad2antrr 758 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) → 𝑈 = {𝑔 ∈ 𝐵 ∣ (𝑔 supp 0 ) ∈ 𝐴}) |
130 | 129 | eleq2d 2673 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) → ((𝑢(+g‘𝑆)𝑣) ∈ 𝑈 ↔ (𝑢(+g‘𝑆)𝑣) ∈ {𝑔 ∈ 𝐵 ∣ (𝑔 supp 0 ) ∈ 𝐴})) |
131 | | oveq1 6556 |
. . . . . . . . 9
⊢ (𝑔 = (𝑢(+g‘𝑆)𝑣) → (𝑔 supp 0 ) = ((𝑢(+g‘𝑆)𝑣) supp 0 )) |
132 | 131 | eleq1d 2672 |
. . . . . . . 8
⊢ (𝑔 = (𝑢(+g‘𝑆)𝑣) → ((𝑔 supp 0 ) ∈ 𝐴 ↔ ((𝑢(+g‘𝑆)𝑣) supp 0 ) ∈ 𝐴)) |
133 | 132 | elrab 3331 |
. . . . . . 7
⊢ ((𝑢(+g‘𝑆)𝑣) ∈ {𝑔 ∈ 𝐵 ∣ (𝑔 supp 0 ) ∈ 𝐴} ↔ ((𝑢(+g‘𝑆)𝑣) ∈ 𝐵 ∧ ((𝑢(+g‘𝑆)𝑣) supp 0 ) ∈ 𝐴)) |
134 | 130, 133 | syl6bb 275 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) → ((𝑢(+g‘𝑆)𝑣) ∈ 𝑈 ↔ ((𝑢(+g‘𝑆)𝑣) ∈ 𝐵 ∧ ((𝑢(+g‘𝑆)𝑣) supp 0 ) ∈ 𝐴))) |
135 | 52, 128, 134 | mpbir2and 959 |
. . . . 5
⊢ (((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) → (𝑢(+g‘𝑆)𝑣) ∈ 𝑈) |
136 | 135 | ralrimiva 2949 |
. . . 4
⊢ ((𝜑 ∧ 𝑢 ∈ 𝑈) → ∀𝑣 ∈ 𝑈 (𝑢(+g‘𝑆)𝑣) ∈ 𝑈) |
137 | 4, 5, 6 | psrgrp 19219 |
. . . . . 6
⊢ (𝜑 → 𝑆 ∈ Grp) |
138 | | eqid 2610 |
. . . . . . 7
⊢
(invg‘𝑆) = (invg‘𝑆) |
139 | 9, 138 | grpinvcl 17290 |
. . . . . 6
⊢ ((𝑆 ∈ Grp ∧ 𝑢 ∈ 𝐵) → ((invg‘𝑆)‘𝑢) ∈ 𝐵) |
140 | 137, 42, 139 | syl2an2r 872 |
. . . . 5
⊢ ((𝜑 ∧ 𝑢 ∈ 𝑈) → ((invg‘𝑆)‘𝑢) ∈ 𝐵) |
141 | | ovex 6577 |
. . . . . . 7
⊢
(((invg‘𝑆)‘𝑢) supp 0 ) ∈
V |
142 | 141 | a1i 11 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑢 ∈ 𝑈) → (((invg‘𝑆)‘𝑢) supp 0 ) ∈
V) |
143 | 70 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑢 ∈ 𝑈) → ∀𝑥 ∈ 𝐴 ∀𝑦(𝑦 ⊆ 𝑥 → 𝑦 ∈ 𝐴)) |
144 | | sseq2 3590 |
. . . . . . . . . 10
⊢ (𝑥 = (𝑢 supp 0 ) → (𝑦 ⊆ 𝑥 ↔ 𝑦 ⊆ (𝑢 supp 0 ))) |
145 | 144 | imbi1d 330 |
. . . . . . . . 9
⊢ (𝑥 = (𝑢 supp 0 ) → ((𝑦 ⊆ 𝑥 → 𝑦 ∈ 𝐴) ↔ (𝑦 ⊆ (𝑢 supp 0 ) → 𝑦 ∈ 𝐴))) |
146 | 145 | albidv 1836 |
. . . . . . . 8
⊢ (𝑥 = (𝑢 supp 0 ) → (∀𝑦(𝑦 ⊆ 𝑥 → 𝑦 ∈ 𝐴) ↔ ∀𝑦(𝑦 ⊆ (𝑢 supp 0 ) → 𝑦 ∈ 𝐴))) |
147 | 146 | rspcv 3278 |
. . . . . . 7
⊢ ((𝑢 supp 0 ) ∈ 𝐴 → (∀𝑥 ∈ 𝐴 ∀𝑦(𝑦 ⊆ 𝑥 → 𝑦 ∈ 𝐴) → ∀𝑦(𝑦 ⊆ (𝑢 supp 0 ) → 𝑦 ∈ 𝐴))) |
148 | 55, 143, 147 | sylc 63 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑢 ∈ 𝑈) → ∀𝑦(𝑦 ⊆ (𝑢 supp 0 ) → 𝑦 ∈ 𝐴)) |
149 | 4, 11, 7, 9, 140 | psrelbas 19200 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑢 ∈ 𝑈) → ((invg‘𝑆)‘𝑢):𝐷⟶(Base‘𝑅)) |
150 | 5 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑢 ∈ 𝑈) → 𝐼 ∈ 𝑊) |
151 | 6 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑢 ∈ 𝑈) → 𝑅 ∈ Grp) |
152 | | eqid 2610 |
. . . . . . . . . . 11
⊢
(invg‘𝑅) = (invg‘𝑅) |
153 | 4, 150, 151, 7, 152, 9, 138, 42 | psrneg 19221 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑢 ∈ 𝑈) → ((invg‘𝑆)‘𝑢) = ((invg‘𝑅) ∘ 𝑢)) |
154 | 153 | adantr 480 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑘 ∈ (𝐷 ∖ (𝑢 supp 0 ))) →
((invg‘𝑆)‘𝑢) = ((invg‘𝑅) ∘ 𝑢)) |
155 | 154 | fveq1d 6105 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑘 ∈ (𝐷 ∖ (𝑢 supp 0 ))) →
(((invg‘𝑆)‘𝑢)‘𝑘) = (((invg‘𝑅) ∘ 𝑢)‘𝑘)) |
156 | | eldifi 3694 |
. . . . . . . . 9
⊢ (𝑘 ∈ (𝐷 ∖ (𝑢 supp 0 )) → 𝑘 ∈ 𝐷) |
157 | | fvco3 6185 |
. . . . . . . . 9
⊢ ((𝑢:𝐷⟶(Base‘𝑅) ∧ 𝑘 ∈ 𝐷) → (((invg‘𝑅) ∘ 𝑢)‘𝑘) = ((invg‘𝑅)‘(𝑢‘𝑘))) |
158 | 83, 156, 157 | syl2an 493 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑘 ∈ (𝐷 ∖ (𝑢 supp 0 ))) →
(((invg‘𝑅)
∘ 𝑢)‘𝑘) =
((invg‘𝑅)‘(𝑢‘𝑘))) |
159 | 104 | fveq2d 6107 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑘 ∈ (𝐷 ∖ (𝑢 supp 0 ))) →
((invg‘𝑅)‘(𝑢‘𝑘)) = ((invg‘𝑅)‘ 0 )) |
160 | 8, 152 | grpinvid 17299 |
. . . . . . . . . . 11
⊢ (𝑅 ∈ Grp →
((invg‘𝑅)‘ 0 ) = 0 ) |
161 | 151, 160 | syl 17 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑢 ∈ 𝑈) → ((invg‘𝑅)‘ 0 ) = 0 ) |
162 | 161 | adantr 480 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑘 ∈ (𝐷 ∖ (𝑢 supp 0 ))) →
((invg‘𝑅)‘ 0 ) = 0 ) |
163 | 159, 162 | eqtrd 2644 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑘 ∈ (𝐷 ∖ (𝑢 supp 0 ))) →
((invg‘𝑅)‘(𝑢‘𝑘)) = 0 ) |
164 | 155, 158,
163 | 3eqtrd 2648 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑘 ∈ (𝐷 ∖ (𝑢 supp 0 ))) →
(((invg‘𝑆)‘𝑢)‘𝑘) = 0 ) |
165 | 149, 164 | suppss 7212 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑢 ∈ 𝑈) → (((invg‘𝑆)‘𝑢) supp 0 ) ⊆ (𝑢 supp 0 )) |
166 | | sseq1 3589 |
. . . . . . . 8
⊢ (𝑦 =
(((invg‘𝑆)‘𝑢) supp 0 ) → (𝑦 ⊆ (𝑢 supp 0 ) ↔
(((invg‘𝑆)‘𝑢) supp 0 ) ⊆ (𝑢 supp 0 ))) |
167 | | eleq1 2676 |
. . . . . . . 8
⊢ (𝑦 =
(((invg‘𝑆)‘𝑢) supp 0 ) → (𝑦 ∈ 𝐴 ↔ (((invg‘𝑆)‘𝑢) supp 0 ) ∈ 𝐴)) |
168 | 166, 167 | imbi12d 333 |
. . . . . . 7
⊢ (𝑦 =
(((invg‘𝑆)‘𝑢) supp 0 ) → ((𝑦 ⊆ (𝑢 supp 0 ) → 𝑦 ∈ 𝐴) ↔ ((((invg‘𝑆)‘𝑢) supp 0 ) ⊆ (𝑢 supp 0 ) →
(((invg‘𝑆)‘𝑢) supp 0 ) ∈ 𝐴))) |
169 | 168 | spcgv 3266 |
. . . . . 6
⊢
((((invg‘𝑆)‘𝑢) supp 0 ) ∈ V →
(∀𝑦(𝑦 ⊆ (𝑢 supp 0 ) → 𝑦 ∈ 𝐴) → ((((invg‘𝑆)‘𝑢) supp 0 ) ⊆ (𝑢 supp 0 ) →
(((invg‘𝑆)‘𝑢) supp 0 ) ∈ 𝐴))) |
170 | 142, 148,
165, 169 | syl3c 64 |
. . . . 5
⊢ ((𝜑 ∧ 𝑢 ∈ 𝑈) → (((invg‘𝑆)‘𝑢) supp 0 ) ∈ 𝐴) |
171 | 44 | eleq2d 2673 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑢 ∈ 𝑈) → (((invg‘𝑆)‘𝑢) ∈ 𝑈 ↔ ((invg‘𝑆)‘𝑢) ∈ {𝑔 ∈ 𝐵 ∣ (𝑔 supp 0 ) ∈ 𝐴})) |
172 | | oveq1 6556 |
. . . . . . . 8
⊢ (𝑔 = ((invg‘𝑆)‘𝑢) → (𝑔 supp 0 ) =
(((invg‘𝑆)‘𝑢) supp 0 )) |
173 | 172 | eleq1d 2672 |
. . . . . . 7
⊢ (𝑔 = ((invg‘𝑆)‘𝑢) → ((𝑔 supp 0 ) ∈ 𝐴 ↔ (((invg‘𝑆)‘𝑢) supp 0 ) ∈ 𝐴)) |
174 | 173 | elrab 3331 |
. . . . . 6
⊢
(((invg‘𝑆)‘𝑢) ∈ {𝑔 ∈ 𝐵 ∣ (𝑔 supp 0 ) ∈ 𝐴} ↔ (((invg‘𝑆)‘𝑢) ∈ 𝐵 ∧ (((invg‘𝑆)‘𝑢) supp 0 ) ∈ 𝐴)) |
175 | 171, 174 | syl6bb 275 |
. . . . 5
⊢ ((𝜑 ∧ 𝑢 ∈ 𝑈) → (((invg‘𝑆)‘𝑢) ∈ 𝑈 ↔ (((invg‘𝑆)‘𝑢) ∈ 𝐵 ∧ (((invg‘𝑆)‘𝑢) supp 0 ) ∈ 𝐴))) |
176 | 140, 170,
175 | mpbir2and 959 |
. . . 4
⊢ ((𝜑 ∧ 𝑢 ∈ 𝑈) → ((invg‘𝑆)‘𝑢) ∈ 𝑈) |
177 | 136, 176 | jca 553 |
. . 3
⊢ ((𝜑 ∧ 𝑢 ∈ 𝑈) → (∀𝑣 ∈ 𝑈 (𝑢(+g‘𝑆)𝑣) ∈ 𝑈 ∧ ((invg‘𝑆)‘𝑢) ∈ 𝑈)) |
178 | 177 | ralrimiva 2949 |
. 2
⊢ (𝜑 → ∀𝑢 ∈ 𝑈 (∀𝑣 ∈ 𝑈 (𝑢(+g‘𝑆)𝑣) ∈ 𝑈 ∧ ((invg‘𝑆)‘𝑢) ∈ 𝑈)) |
179 | 9, 34, 138 | issubg2 17432 |
. . 3
⊢ (𝑆 ∈ Grp → (𝑈 ∈ (SubGrp‘𝑆) ↔ (𝑈 ⊆ 𝐵 ∧ 𝑈 ≠ ∅ ∧ ∀𝑢 ∈ 𝑈 (∀𝑣 ∈ 𝑈 (𝑢(+g‘𝑆)𝑣) ∈ 𝑈 ∧ ((invg‘𝑆)‘𝑢) ∈ 𝑈)))) |
180 | 137, 179 | syl 17 |
. 2
⊢ (𝜑 → (𝑈 ∈ (SubGrp‘𝑆) ↔ (𝑈 ⊆ 𝐵 ∧ 𝑈 ≠ ∅ ∧ ∀𝑢 ∈ 𝑈 (∀𝑣 ∈ 𝑈 (𝑢(+g‘𝑆)𝑣) ∈ 𝑈 ∧ ((invg‘𝑆)‘𝑢) ∈ 𝑈)))) |
181 | 3, 33, 178, 180 | mpbir3and 1238 |
1
⊢ (𝜑 → 𝑈 ∈ (SubGrp‘𝑆)) |