| Step | Hyp | Ref
| Expression |
| 1 | | lsmcntz.s |
. . . . . . 7
⊢ (𝜑 → 𝑆 ∈ (SubGrp‘𝐺)) |
| 2 | | lsmcntz.u |
. . . . . . 7
⊢ (𝜑 → 𝑈 ∈ (SubGrp‘𝐺)) |
| 3 | | eqid 2737 |
. . . . . . . 8
⊢
(+g‘𝐺) = (+g‘𝐺) |
| 4 | | lsmcntz.p |
. . . . . . . 8
⊢ ⊕ =
(LSSum‘𝐺) |
| 5 | 3, 4 | lsmelval 19667 |
. . . . . . 7
⊢ ((𝑆 ∈ (SubGrp‘𝐺) ∧ 𝑈 ∈ (SubGrp‘𝐺)) → (𝑥 ∈ (𝑆 ⊕ 𝑈) ↔ ∃𝑠 ∈ 𝑆 ∃𝑢 ∈ 𝑈 𝑥 = (𝑠(+g‘𝐺)𝑢))) |
| 6 | 1, 2, 5 | syl2anc 584 |
. . . . . 6
⊢ (𝜑 → (𝑥 ∈ (𝑆 ⊕ 𝑈) ↔ ∃𝑠 ∈ 𝑆 ∃𝑢 ∈ 𝑈 𝑥 = (𝑠(+g‘𝐺)𝑢))) |
| 7 | | simplrl 777 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑠 ∈ 𝑆 ∧ 𝑢 ∈ 𝑈)) ∧ (𝑠(+g‘𝐺)𝑢) ∈ 𝑇) → 𝑠 ∈ 𝑆) |
| 8 | | subgrcl 19149 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑆 ∈ (SubGrp‘𝐺) → 𝐺 ∈ Grp) |
| 9 | 1, 8 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝜑 → 𝐺 ∈ Grp) |
| 10 | 9 | ad2antrr 726 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝜑 ∧ (𝑠 ∈ 𝑆 ∧ 𝑢 ∈ 𝑈)) ∧ (𝑠(+g‘𝐺)𝑢) ∈ 𝑇) → 𝐺 ∈ Grp) |
| 11 | 1 | ad2antrr 726 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝜑 ∧ (𝑠 ∈ 𝑆 ∧ 𝑢 ∈ 𝑈)) ∧ (𝑠(+g‘𝐺)𝑢) ∈ 𝑇) → 𝑆 ∈ (SubGrp‘𝐺)) |
| 12 | | eqid 2737 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
(Base‘𝐺) =
(Base‘𝐺) |
| 13 | 12 | subgss 19145 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑆 ∈ (SubGrp‘𝐺) → 𝑆 ⊆ (Base‘𝐺)) |
| 14 | 11, 13 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝜑 ∧ (𝑠 ∈ 𝑆 ∧ 𝑢 ∈ 𝑈)) ∧ (𝑠(+g‘𝐺)𝑢) ∈ 𝑇) → 𝑆 ⊆ (Base‘𝐺)) |
| 15 | 14, 7 | sseldd 3984 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝜑 ∧ (𝑠 ∈ 𝑆 ∧ 𝑢 ∈ 𝑈)) ∧ (𝑠(+g‘𝐺)𝑢) ∈ 𝑇) → 𝑠 ∈ (Base‘𝐺)) |
| 16 | | lsmdisj.o |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ 0 =
(0g‘𝐺) |
| 17 | | eqid 2737 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
(invg‘𝐺) = (invg‘𝐺) |
| 18 | 12, 3, 16, 17 | grplinv 19007 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝐺 ∈ Grp ∧ 𝑠 ∈ (Base‘𝐺)) →
(((invg‘𝐺)‘𝑠)(+g‘𝐺)𝑠) = 0 ) |
| 19 | 10, 15, 18 | syl2anc 584 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝜑 ∧ (𝑠 ∈ 𝑆 ∧ 𝑢 ∈ 𝑈)) ∧ (𝑠(+g‘𝐺)𝑢) ∈ 𝑇) → (((invg‘𝐺)‘𝑠)(+g‘𝐺)𝑠) = 0 ) |
| 20 | 19 | oveq1d 7446 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ (𝑠 ∈ 𝑆 ∧ 𝑢 ∈ 𝑈)) ∧ (𝑠(+g‘𝐺)𝑢) ∈ 𝑇) → ((((invg‘𝐺)‘𝑠)(+g‘𝐺)𝑠)(+g‘𝐺)𝑢) = ( 0 (+g‘𝐺)𝑢)) |
| 21 | 17 | subginvcl 19153 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑆 ∈ (SubGrp‘𝐺) ∧ 𝑠 ∈ 𝑆) → ((invg‘𝐺)‘𝑠) ∈ 𝑆) |
| 22 | 11, 7, 21 | syl2anc 584 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝜑 ∧ (𝑠 ∈ 𝑆 ∧ 𝑢 ∈ 𝑈)) ∧ (𝑠(+g‘𝐺)𝑢) ∈ 𝑇) → ((invg‘𝐺)‘𝑠) ∈ 𝑆) |
| 23 | 14, 22 | sseldd 3984 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝜑 ∧ (𝑠 ∈ 𝑆 ∧ 𝑢 ∈ 𝑈)) ∧ (𝑠(+g‘𝐺)𝑢) ∈ 𝑇) → ((invg‘𝐺)‘𝑠) ∈ (Base‘𝐺)) |
| 24 | 2 | ad2antrr 726 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝜑 ∧ (𝑠 ∈ 𝑆 ∧ 𝑢 ∈ 𝑈)) ∧ (𝑠(+g‘𝐺)𝑢) ∈ 𝑇) → 𝑈 ∈ (SubGrp‘𝐺)) |
| 25 | 12 | subgss 19145 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑈 ∈ (SubGrp‘𝐺) → 𝑈 ⊆ (Base‘𝐺)) |
| 26 | 24, 25 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝜑 ∧ (𝑠 ∈ 𝑆 ∧ 𝑢 ∈ 𝑈)) ∧ (𝑠(+g‘𝐺)𝑢) ∈ 𝑇) → 𝑈 ⊆ (Base‘𝐺)) |
| 27 | | simplrr 778 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝜑 ∧ (𝑠 ∈ 𝑆 ∧ 𝑢 ∈ 𝑈)) ∧ (𝑠(+g‘𝐺)𝑢) ∈ 𝑇) → 𝑢 ∈ 𝑈) |
| 28 | 26, 27 | sseldd 3984 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝜑 ∧ (𝑠 ∈ 𝑆 ∧ 𝑢 ∈ 𝑈)) ∧ (𝑠(+g‘𝐺)𝑢) ∈ 𝑇) → 𝑢 ∈ (Base‘𝐺)) |
| 29 | 12, 3 | grpass 18960 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝐺 ∈ Grp ∧
(((invg‘𝐺)‘𝑠) ∈ (Base‘𝐺) ∧ 𝑠 ∈ (Base‘𝐺) ∧ 𝑢 ∈ (Base‘𝐺))) → ((((invg‘𝐺)‘𝑠)(+g‘𝐺)𝑠)(+g‘𝐺)𝑢) = (((invg‘𝐺)‘𝑠)(+g‘𝐺)(𝑠(+g‘𝐺)𝑢))) |
| 30 | 10, 23, 15, 28, 29 | syl13anc 1374 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ (𝑠 ∈ 𝑆 ∧ 𝑢 ∈ 𝑈)) ∧ (𝑠(+g‘𝐺)𝑢) ∈ 𝑇) → ((((invg‘𝐺)‘𝑠)(+g‘𝐺)𝑠)(+g‘𝐺)𝑢) = (((invg‘𝐺)‘𝑠)(+g‘𝐺)(𝑠(+g‘𝐺)𝑢))) |
| 31 | 12, 3, 16 | grplid 18985 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝐺 ∈ Grp ∧ 𝑢 ∈ (Base‘𝐺)) → ( 0 (+g‘𝐺)𝑢) = 𝑢) |
| 32 | 10, 28, 31 | syl2anc 584 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ (𝑠 ∈ 𝑆 ∧ 𝑢 ∈ 𝑈)) ∧ (𝑠(+g‘𝐺)𝑢) ∈ 𝑇) → ( 0 (+g‘𝐺)𝑢) = 𝑢) |
| 33 | 20, 30, 32 | 3eqtr3d 2785 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ (𝑠 ∈ 𝑆 ∧ 𝑢 ∈ 𝑈)) ∧ (𝑠(+g‘𝐺)𝑢) ∈ 𝑇) → (((invg‘𝐺)‘𝑠)(+g‘𝐺)(𝑠(+g‘𝐺)𝑢)) = 𝑢) |
| 34 | | lsmcntz.t |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜑 → 𝑇 ∈ (SubGrp‘𝐺)) |
| 35 | 34 | ad2antrr 726 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ (𝑠 ∈ 𝑆 ∧ 𝑢 ∈ 𝑈)) ∧ (𝑠(+g‘𝐺)𝑢) ∈ 𝑇) → 𝑇 ∈ (SubGrp‘𝐺)) |
| 36 | | simpr 484 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ (𝑠 ∈ 𝑆 ∧ 𝑢 ∈ 𝑈)) ∧ (𝑠(+g‘𝐺)𝑢) ∈ 𝑇) → (𝑠(+g‘𝐺)𝑢) ∈ 𝑇) |
| 37 | 3, 4 | lsmelvali 19668 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝑆 ∈ (SubGrp‘𝐺) ∧ 𝑇 ∈ (SubGrp‘𝐺)) ∧ (((invg‘𝐺)‘𝑠) ∈ 𝑆 ∧ (𝑠(+g‘𝐺)𝑢) ∈ 𝑇)) → (((invg‘𝐺)‘𝑠)(+g‘𝐺)(𝑠(+g‘𝐺)𝑢)) ∈ (𝑆 ⊕ 𝑇)) |
| 38 | 11, 35, 22, 36, 37 | syl22anc 839 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ (𝑠 ∈ 𝑆 ∧ 𝑢 ∈ 𝑈)) ∧ (𝑠(+g‘𝐺)𝑢) ∈ 𝑇) → (((invg‘𝐺)‘𝑠)(+g‘𝐺)(𝑠(+g‘𝐺)𝑢)) ∈ (𝑆 ⊕ 𝑇)) |
| 39 | 33, 38 | eqeltrrd 2842 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ (𝑠 ∈ 𝑆 ∧ 𝑢 ∈ 𝑈)) ∧ (𝑠(+g‘𝐺)𝑢) ∈ 𝑇) → 𝑢 ∈ (𝑆 ⊕ 𝑇)) |
| 40 | 39, 27 | elind 4200 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ (𝑠 ∈ 𝑆 ∧ 𝑢 ∈ 𝑈)) ∧ (𝑠(+g‘𝐺)𝑢) ∈ 𝑇) → 𝑢 ∈ ((𝑆 ⊕ 𝑇) ∩ 𝑈)) |
| 41 | | lsmdisj.i |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → ((𝑆 ⊕ 𝑇) ∩ 𝑈) = { 0 }) |
| 42 | 41 | ad2antrr 726 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ (𝑠 ∈ 𝑆 ∧ 𝑢 ∈ 𝑈)) ∧ (𝑠(+g‘𝐺)𝑢) ∈ 𝑇) → ((𝑆 ⊕ 𝑇) ∩ 𝑈) = { 0 }) |
| 43 | 40, 42 | eleqtrd 2843 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ (𝑠 ∈ 𝑆 ∧ 𝑢 ∈ 𝑈)) ∧ (𝑠(+g‘𝐺)𝑢) ∈ 𝑇) → 𝑢 ∈ { 0 }) |
| 44 | | elsni 4643 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑢 ∈ { 0 } → 𝑢 = 0 ) |
| 45 | 43, 44 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ (𝑠 ∈ 𝑆 ∧ 𝑢 ∈ 𝑈)) ∧ (𝑠(+g‘𝐺)𝑢) ∈ 𝑇) → 𝑢 = 0 ) |
| 46 | 45 | oveq2d 7447 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑠 ∈ 𝑆 ∧ 𝑢 ∈ 𝑈)) ∧ (𝑠(+g‘𝐺)𝑢) ∈ 𝑇) → (𝑠(+g‘𝐺)𝑢) = (𝑠(+g‘𝐺) 0 )) |
| 47 | 12, 3, 16 | grprid 18986 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐺 ∈ Grp ∧ 𝑠 ∈ (Base‘𝐺)) → (𝑠(+g‘𝐺) 0 ) = 𝑠) |
| 48 | 10, 15, 47 | syl2anc 584 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑠 ∈ 𝑆 ∧ 𝑢 ∈ 𝑈)) ∧ (𝑠(+g‘𝐺)𝑢) ∈ 𝑇) → (𝑠(+g‘𝐺) 0 ) = 𝑠) |
| 49 | 46, 48 | eqtrd 2777 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑠 ∈ 𝑆 ∧ 𝑢 ∈ 𝑈)) ∧ (𝑠(+g‘𝐺)𝑢) ∈ 𝑇) → (𝑠(+g‘𝐺)𝑢) = 𝑠) |
| 50 | 49, 36 | eqeltrrd 2842 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑠 ∈ 𝑆 ∧ 𝑢 ∈ 𝑈)) ∧ (𝑠(+g‘𝐺)𝑢) ∈ 𝑇) → 𝑠 ∈ 𝑇) |
| 51 | 7, 50 | elind 4200 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑠 ∈ 𝑆 ∧ 𝑢 ∈ 𝑈)) ∧ (𝑠(+g‘𝐺)𝑢) ∈ 𝑇) → 𝑠 ∈ (𝑆 ∩ 𝑇)) |
| 52 | | lsmdisj2.i |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑆 ∩ 𝑇) = { 0 }) |
| 53 | 52 | ad2antrr 726 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑠 ∈ 𝑆 ∧ 𝑢 ∈ 𝑈)) ∧ (𝑠(+g‘𝐺)𝑢) ∈ 𝑇) → (𝑆 ∩ 𝑇) = { 0 }) |
| 54 | 51, 53 | eleqtrd 2843 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑠 ∈ 𝑆 ∧ 𝑢 ∈ 𝑈)) ∧ (𝑠(+g‘𝐺)𝑢) ∈ 𝑇) → 𝑠 ∈ { 0 }) |
| 55 | | elsni 4643 |
. . . . . . . . . . . 12
⊢ (𝑠 ∈ { 0 } → 𝑠 = 0 ) |
| 56 | 54, 55 | syl 17 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑠 ∈ 𝑆 ∧ 𝑢 ∈ 𝑈)) ∧ (𝑠(+g‘𝐺)𝑢) ∈ 𝑇) → 𝑠 = 0 ) |
| 57 | 56, 45 | oveq12d 7449 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑠 ∈ 𝑆 ∧ 𝑢 ∈ 𝑈)) ∧ (𝑠(+g‘𝐺)𝑢) ∈ 𝑇) → (𝑠(+g‘𝐺)𝑢) = ( 0 (+g‘𝐺) 0 )) |
| 58 | 12, 16 | grpidcl 18983 |
. . . . . . . . . . . 12
⊢ (𝐺 ∈ Grp → 0 ∈
(Base‘𝐺)) |
| 59 | 12, 3, 16 | grplid 18985 |
. . . . . . . . . . . 12
⊢ ((𝐺 ∈ Grp ∧ 0 ∈
(Base‘𝐺)) → (
0
(+g‘𝐺)
0 ) =
0
) |
| 60 | 9, 58, 59 | syl2anc2 585 |
. . . . . . . . . . 11
⊢ (𝜑 → ( 0 (+g‘𝐺) 0 ) = 0 ) |
| 61 | 60 | ad2antrr 726 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑠 ∈ 𝑆 ∧ 𝑢 ∈ 𝑈)) ∧ (𝑠(+g‘𝐺)𝑢) ∈ 𝑇) → ( 0 (+g‘𝐺) 0 ) = 0 ) |
| 62 | 57, 61 | eqtrd 2777 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑠 ∈ 𝑆 ∧ 𝑢 ∈ 𝑈)) ∧ (𝑠(+g‘𝐺)𝑢) ∈ 𝑇) → (𝑠(+g‘𝐺)𝑢) = 0 ) |
| 63 | 62 | ex 412 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑠 ∈ 𝑆 ∧ 𝑢 ∈ 𝑈)) → ((𝑠(+g‘𝐺)𝑢) ∈ 𝑇 → (𝑠(+g‘𝐺)𝑢) = 0 )) |
| 64 | | eleq1 2829 |
. . . . . . . . 9
⊢ (𝑥 = (𝑠(+g‘𝐺)𝑢) → (𝑥 ∈ 𝑇 ↔ (𝑠(+g‘𝐺)𝑢) ∈ 𝑇)) |
| 65 | | eqeq1 2741 |
. . . . . . . . 9
⊢ (𝑥 = (𝑠(+g‘𝐺)𝑢) → (𝑥 = 0 ↔ (𝑠(+g‘𝐺)𝑢) = 0 )) |
| 66 | 64, 65 | imbi12d 344 |
. . . . . . . 8
⊢ (𝑥 = (𝑠(+g‘𝐺)𝑢) → ((𝑥 ∈ 𝑇 → 𝑥 = 0 ) ↔ ((𝑠(+g‘𝐺)𝑢) ∈ 𝑇 → (𝑠(+g‘𝐺)𝑢) = 0 ))) |
| 67 | 63, 66 | syl5ibrcom 247 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑠 ∈ 𝑆 ∧ 𝑢 ∈ 𝑈)) → (𝑥 = (𝑠(+g‘𝐺)𝑢) → (𝑥 ∈ 𝑇 → 𝑥 = 0 ))) |
| 68 | 67 | rexlimdvva 3213 |
. . . . . 6
⊢ (𝜑 → (∃𝑠 ∈ 𝑆 ∃𝑢 ∈ 𝑈 𝑥 = (𝑠(+g‘𝐺)𝑢) → (𝑥 ∈ 𝑇 → 𝑥 = 0 ))) |
| 69 | 6, 68 | sylbid 240 |
. . . . 5
⊢ (𝜑 → (𝑥 ∈ (𝑆 ⊕ 𝑈) → (𝑥 ∈ 𝑇 → 𝑥 = 0 ))) |
| 70 | 69 | impcomd 411 |
. . . 4
⊢ (𝜑 → ((𝑥 ∈ 𝑇 ∧ 𝑥 ∈ (𝑆 ⊕ 𝑈)) → 𝑥 = 0 )) |
| 71 | | elin 3967 |
. . . 4
⊢ (𝑥 ∈ (𝑇 ∩ (𝑆 ⊕ 𝑈)) ↔ (𝑥 ∈ 𝑇 ∧ 𝑥 ∈ (𝑆 ⊕ 𝑈))) |
| 72 | | velsn 4642 |
. . . 4
⊢ (𝑥 ∈ { 0 } ↔ 𝑥 = 0 ) |
| 73 | 70, 71, 72 | 3imtr4g 296 |
. . 3
⊢ (𝜑 → (𝑥 ∈ (𝑇 ∩ (𝑆 ⊕ 𝑈)) → 𝑥 ∈ { 0 })) |
| 74 | 73 | ssrdv 3989 |
. 2
⊢ (𝜑 → (𝑇 ∩ (𝑆 ⊕ 𝑈)) ⊆ { 0 }) |
| 75 | 16 | subg0cl 19152 |
. . . . 5
⊢ (𝑇 ∈ (SubGrp‘𝐺) → 0 ∈ 𝑇) |
| 76 | 34, 75 | syl 17 |
. . . 4
⊢ (𝜑 → 0 ∈ 𝑇) |
| 77 | 4 | lsmub1 19675 |
. . . . . 6
⊢ ((𝑆 ∈ (SubGrp‘𝐺) ∧ 𝑈 ∈ (SubGrp‘𝐺)) → 𝑆 ⊆ (𝑆 ⊕ 𝑈)) |
| 78 | 1, 2, 77 | syl2anc 584 |
. . . . 5
⊢ (𝜑 → 𝑆 ⊆ (𝑆 ⊕ 𝑈)) |
| 79 | 16 | subg0cl 19152 |
. . . . . 6
⊢ (𝑆 ∈ (SubGrp‘𝐺) → 0 ∈ 𝑆) |
| 80 | 1, 79 | syl 17 |
. . . . 5
⊢ (𝜑 → 0 ∈ 𝑆) |
| 81 | 78, 80 | sseldd 3984 |
. . . 4
⊢ (𝜑 → 0 ∈ (𝑆 ⊕ 𝑈)) |
| 82 | 76, 81 | elind 4200 |
. . 3
⊢ (𝜑 → 0 ∈ (𝑇 ∩ (𝑆 ⊕ 𝑈))) |
| 83 | 82 | snssd 4809 |
. 2
⊢ (𝜑 → { 0 } ⊆ (𝑇 ∩ (𝑆 ⊕ 𝑈))) |
| 84 | 74, 83 | eqssd 4001 |
1
⊢ (𝜑 → (𝑇 ∩ (𝑆 ⊕ 𝑈)) = { 0 }) |