Step | Hyp | Ref
| Expression |
1 | | lsmcntz.s |
. . . . . . . 8
⊢ (𝜑 → 𝑆 ∈ (SubGrp‘𝐺)) |
2 | | lsmcntz.u |
. . . . . . . 8
⊢ (𝜑 → 𝑈 ∈ (SubGrp‘𝐺)) |
3 | | eqid 2622 |
. . . . . . . . 9
⊢
(+g‘𝐺) = (+g‘𝐺) |
4 | | lsmcntz.p |
. . . . . . . . 9
⊢ ⊕ =
(LSSum‘𝐺) |
5 | 3, 4 | lsmelval 18064 |
. . . . . . . 8
⊢ ((𝑆 ∈ (SubGrp‘𝐺) ∧ 𝑈 ∈ (SubGrp‘𝐺)) → (𝑥 ∈ (𝑆 ⊕ 𝑈) ↔ ∃𝑠 ∈ 𝑆 ∃𝑢 ∈ 𝑈 𝑥 = (𝑠(+g‘𝐺)𝑢))) |
6 | 1, 2, 5 | syl2anc 693 |
. . . . . . 7
⊢ (𝜑 → (𝑥 ∈ (𝑆 ⊕ 𝑈) ↔ ∃𝑠 ∈ 𝑆 ∃𝑢 ∈ 𝑈 𝑥 = (𝑠(+g‘𝐺)𝑢))) |
7 | | simplrl 800 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑠 ∈ 𝑆 ∧ 𝑢 ∈ 𝑈)) ∧ (𝑠(+g‘𝐺)𝑢) ∈ 𝑇) → 𝑠 ∈ 𝑆) |
8 | | subgrcl 17599 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑆 ∈ (SubGrp‘𝐺) → 𝐺 ∈ Grp) |
9 | 1, 8 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝜑 → 𝐺 ∈ Grp) |
10 | 9 | ad2antrr 762 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝜑 ∧ (𝑠 ∈ 𝑆 ∧ 𝑢 ∈ 𝑈)) ∧ (𝑠(+g‘𝐺)𝑢) ∈ 𝑇) → 𝐺 ∈ Grp) |
11 | 1 | ad2antrr 762 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (((𝜑 ∧ (𝑠 ∈ 𝑆 ∧ 𝑢 ∈ 𝑈)) ∧ (𝑠(+g‘𝐺)𝑢) ∈ 𝑇) → 𝑆 ∈ (SubGrp‘𝐺)) |
12 | | eqid 2622 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
(Base‘𝐺) =
(Base‘𝐺) |
13 | 12 | subgss 17595 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑆 ∈ (SubGrp‘𝐺) → 𝑆 ⊆ (Base‘𝐺)) |
14 | 11, 13 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝜑 ∧ (𝑠 ∈ 𝑆 ∧ 𝑢 ∈ 𝑈)) ∧ (𝑠(+g‘𝐺)𝑢) ∈ 𝑇) → 𝑆 ⊆ (Base‘𝐺)) |
15 | 14, 7 | sseldd 3604 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝜑 ∧ (𝑠 ∈ 𝑆 ∧ 𝑢 ∈ 𝑈)) ∧ (𝑠(+g‘𝐺)𝑢) ∈ 𝑇) → 𝑠 ∈ (Base‘𝐺)) |
16 | | lsmdisj.o |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ 0 =
(0g‘𝐺) |
17 | | eqid 2622 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
(invg‘𝐺) = (invg‘𝐺) |
18 | 12, 3, 16, 17 | grplinv 17468 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝐺 ∈ Grp ∧ 𝑠 ∈ (Base‘𝐺)) →
(((invg‘𝐺)‘𝑠)(+g‘𝐺)𝑠) = 0 ) |
19 | 10, 15, 18 | syl2anc 693 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝜑 ∧ (𝑠 ∈ 𝑆 ∧ 𝑢 ∈ 𝑈)) ∧ (𝑠(+g‘𝐺)𝑢) ∈ 𝑇) → (((invg‘𝐺)‘𝑠)(+g‘𝐺)𝑠) = 0 ) |
20 | 19 | oveq1d 6665 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝜑 ∧ (𝑠 ∈ 𝑆 ∧ 𝑢 ∈ 𝑈)) ∧ (𝑠(+g‘𝐺)𝑢) ∈ 𝑇) → ((((invg‘𝐺)‘𝑠)(+g‘𝐺)𝑠)(+g‘𝐺)𝑢) = ( 0 (+g‘𝐺)𝑢)) |
21 | 17 | subginvcl 17603 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑆 ∈ (SubGrp‘𝐺) ∧ 𝑠 ∈ 𝑆) → ((invg‘𝐺)‘𝑠) ∈ 𝑆) |
22 | 11, 7, 21 | syl2anc 693 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝜑 ∧ (𝑠 ∈ 𝑆 ∧ 𝑢 ∈ 𝑈)) ∧ (𝑠(+g‘𝐺)𝑢) ∈ 𝑇) → ((invg‘𝐺)‘𝑠) ∈ 𝑆) |
23 | 14, 22 | sseldd 3604 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝜑 ∧ (𝑠 ∈ 𝑆 ∧ 𝑢 ∈ 𝑈)) ∧ (𝑠(+g‘𝐺)𝑢) ∈ 𝑇) → ((invg‘𝐺)‘𝑠) ∈ (Base‘𝐺)) |
24 | 2 | ad2antrr 762 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝜑 ∧ (𝑠 ∈ 𝑆 ∧ 𝑢 ∈ 𝑈)) ∧ (𝑠(+g‘𝐺)𝑢) ∈ 𝑇) → 𝑈 ∈ (SubGrp‘𝐺)) |
25 | 12 | subgss 17595 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑈 ∈ (SubGrp‘𝐺) → 𝑈 ⊆ (Base‘𝐺)) |
26 | 24, 25 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝜑 ∧ (𝑠 ∈ 𝑆 ∧ 𝑢 ∈ 𝑈)) ∧ (𝑠(+g‘𝐺)𝑢) ∈ 𝑇) → 𝑈 ⊆ (Base‘𝐺)) |
27 | | simplrr 801 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝜑 ∧ (𝑠 ∈ 𝑆 ∧ 𝑢 ∈ 𝑈)) ∧ (𝑠(+g‘𝐺)𝑢) ∈ 𝑇) → 𝑢 ∈ 𝑈) |
28 | 26, 27 | sseldd 3604 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝜑 ∧ (𝑠 ∈ 𝑆 ∧ 𝑢 ∈ 𝑈)) ∧ (𝑠(+g‘𝐺)𝑢) ∈ 𝑇) → 𝑢 ∈ (Base‘𝐺)) |
29 | 12, 3 | grpass 17431 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝐺 ∈ Grp ∧
(((invg‘𝐺)‘𝑠) ∈ (Base‘𝐺) ∧ 𝑠 ∈ (Base‘𝐺) ∧ 𝑢 ∈ (Base‘𝐺))) → ((((invg‘𝐺)‘𝑠)(+g‘𝐺)𝑠)(+g‘𝐺)𝑢) = (((invg‘𝐺)‘𝑠)(+g‘𝐺)(𝑠(+g‘𝐺)𝑢))) |
30 | 10, 23, 15, 28, 29 | syl13anc 1328 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝜑 ∧ (𝑠 ∈ 𝑆 ∧ 𝑢 ∈ 𝑈)) ∧ (𝑠(+g‘𝐺)𝑢) ∈ 𝑇) → ((((invg‘𝐺)‘𝑠)(+g‘𝐺)𝑠)(+g‘𝐺)𝑢) = (((invg‘𝐺)‘𝑠)(+g‘𝐺)(𝑠(+g‘𝐺)𝑢))) |
31 | 12, 3, 16 | grplid 17452 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝐺 ∈ Grp ∧ 𝑢 ∈ (Base‘𝐺)) → ( 0 (+g‘𝐺)𝑢) = 𝑢) |
32 | 10, 28, 31 | syl2anc 693 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝜑 ∧ (𝑠 ∈ 𝑆 ∧ 𝑢 ∈ 𝑈)) ∧ (𝑠(+g‘𝐺)𝑢) ∈ 𝑇) → ( 0 (+g‘𝐺)𝑢) = 𝑢) |
33 | 20, 30, 32 | 3eqtr3d 2664 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ (𝑠 ∈ 𝑆 ∧ 𝑢 ∈ 𝑈)) ∧ (𝑠(+g‘𝐺)𝑢) ∈ 𝑇) → (((invg‘𝐺)‘𝑠)(+g‘𝐺)(𝑠(+g‘𝐺)𝑢)) = 𝑢) |
34 | | lsmcntz.t |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝜑 → 𝑇 ∈ (SubGrp‘𝐺)) |
35 | 34 | ad2antrr 762 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝜑 ∧ (𝑠 ∈ 𝑆 ∧ 𝑢 ∈ 𝑈)) ∧ (𝑠(+g‘𝐺)𝑢) ∈ 𝑇) → 𝑇 ∈ (SubGrp‘𝐺)) |
36 | | simpr 477 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝜑 ∧ (𝑠 ∈ 𝑆 ∧ 𝑢 ∈ 𝑈)) ∧ (𝑠(+g‘𝐺)𝑢) ∈ 𝑇) → (𝑠(+g‘𝐺)𝑢) ∈ 𝑇) |
37 | 3, 4 | lsmelvali 18065 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝑆 ∈ (SubGrp‘𝐺) ∧ 𝑇 ∈ (SubGrp‘𝐺)) ∧ (((invg‘𝐺)‘𝑠) ∈ 𝑆 ∧ (𝑠(+g‘𝐺)𝑢) ∈ 𝑇)) → (((invg‘𝐺)‘𝑠)(+g‘𝐺)(𝑠(+g‘𝐺)𝑢)) ∈ (𝑆 ⊕ 𝑇)) |
38 | 11, 35, 22, 36, 37 | syl22anc 1327 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ (𝑠 ∈ 𝑆 ∧ 𝑢 ∈ 𝑈)) ∧ (𝑠(+g‘𝐺)𝑢) ∈ 𝑇) → (((invg‘𝐺)‘𝑠)(+g‘𝐺)(𝑠(+g‘𝐺)𝑢)) ∈ (𝑆 ⊕ 𝑇)) |
39 | 33, 38 | eqeltrrd 2702 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ (𝑠 ∈ 𝑆 ∧ 𝑢 ∈ 𝑈)) ∧ (𝑠(+g‘𝐺)𝑢) ∈ 𝑇) → 𝑢 ∈ (𝑆 ⊕ 𝑇)) |
40 | 39, 27 | elind 3798 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ (𝑠 ∈ 𝑆 ∧ 𝑢 ∈ 𝑈)) ∧ (𝑠(+g‘𝐺)𝑢) ∈ 𝑇) → 𝑢 ∈ ((𝑆 ⊕ 𝑇) ∩ 𝑈)) |
41 | | lsmdisj.i |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → ((𝑆 ⊕ 𝑇) ∩ 𝑈) = { 0 }) |
42 | 41 | ad2antrr 762 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ (𝑠 ∈ 𝑆 ∧ 𝑢 ∈ 𝑈)) ∧ (𝑠(+g‘𝐺)𝑢) ∈ 𝑇) → ((𝑆 ⊕ 𝑇) ∩ 𝑈) = { 0 }) |
43 | 40, 42 | eleqtrd 2703 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ (𝑠 ∈ 𝑆 ∧ 𝑢 ∈ 𝑈)) ∧ (𝑠(+g‘𝐺)𝑢) ∈ 𝑇) → 𝑢 ∈ { 0 }) |
44 | | elsni 4194 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑢 ∈ { 0 } → 𝑢 = 0 ) |
45 | 43, 44 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ (𝑠 ∈ 𝑆 ∧ 𝑢 ∈ 𝑈)) ∧ (𝑠(+g‘𝐺)𝑢) ∈ 𝑇) → 𝑢 = 0 ) |
46 | 45 | oveq2d 6666 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ (𝑠 ∈ 𝑆 ∧ 𝑢 ∈ 𝑈)) ∧ (𝑠(+g‘𝐺)𝑢) ∈ 𝑇) → (𝑠(+g‘𝐺)𝑢) = (𝑠(+g‘𝐺) 0 )) |
47 | 12, 3, 16 | grprid 17453 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐺 ∈ Grp ∧ 𝑠 ∈ (Base‘𝐺)) → (𝑠(+g‘𝐺) 0 ) = 𝑠) |
48 | 10, 15, 47 | syl2anc 693 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ (𝑠 ∈ 𝑆 ∧ 𝑢 ∈ 𝑈)) ∧ (𝑠(+g‘𝐺)𝑢) ∈ 𝑇) → (𝑠(+g‘𝐺) 0 ) = 𝑠) |
49 | 46, 48 | eqtrd 2656 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑠 ∈ 𝑆 ∧ 𝑢 ∈ 𝑈)) ∧ (𝑠(+g‘𝐺)𝑢) ∈ 𝑇) → (𝑠(+g‘𝐺)𝑢) = 𝑠) |
50 | 49, 36 | eqeltrrd 2702 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑠 ∈ 𝑆 ∧ 𝑢 ∈ 𝑈)) ∧ (𝑠(+g‘𝐺)𝑢) ∈ 𝑇) → 𝑠 ∈ 𝑇) |
51 | 7, 50 | elind 3798 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑠 ∈ 𝑆 ∧ 𝑢 ∈ 𝑈)) ∧ (𝑠(+g‘𝐺)𝑢) ∈ 𝑇) → 𝑠 ∈ (𝑆 ∩ 𝑇)) |
52 | | lsmdisj2.i |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝑆 ∩ 𝑇) = { 0 }) |
53 | 52 | ad2antrr 762 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑠 ∈ 𝑆 ∧ 𝑢 ∈ 𝑈)) ∧ (𝑠(+g‘𝐺)𝑢) ∈ 𝑇) → (𝑆 ∩ 𝑇) = { 0 }) |
54 | 51, 53 | eleqtrd 2703 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑠 ∈ 𝑆 ∧ 𝑢 ∈ 𝑈)) ∧ (𝑠(+g‘𝐺)𝑢) ∈ 𝑇) → 𝑠 ∈ { 0 }) |
55 | | elsni 4194 |
. . . . . . . . . . . . 13
⊢ (𝑠 ∈ { 0 } → 𝑠 = 0 ) |
56 | 54, 55 | syl 17 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑠 ∈ 𝑆 ∧ 𝑢 ∈ 𝑈)) ∧ (𝑠(+g‘𝐺)𝑢) ∈ 𝑇) → 𝑠 = 0 ) |
57 | 56, 45 | oveq12d 6668 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑠 ∈ 𝑆 ∧ 𝑢 ∈ 𝑈)) ∧ (𝑠(+g‘𝐺)𝑢) ∈ 𝑇) → (𝑠(+g‘𝐺)𝑢) = ( 0 (+g‘𝐺) 0 )) |
58 | 12, 16 | grpidcl 17450 |
. . . . . . . . . . . . . 14
⊢ (𝐺 ∈ Grp → 0 ∈
(Base‘𝐺)) |
59 | 9, 58 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 0 ∈ (Base‘𝐺)) |
60 | 12, 3, 16 | grplid 17452 |
. . . . . . . . . . . . 13
⊢ ((𝐺 ∈ Grp ∧ 0 ∈
(Base‘𝐺)) → (
0
(+g‘𝐺)
0 ) =
0
) |
61 | 9, 59, 60 | syl2anc 693 |
. . . . . . . . . . . 12
⊢ (𝜑 → ( 0 (+g‘𝐺) 0 ) = 0 ) |
62 | 61 | ad2antrr 762 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑠 ∈ 𝑆 ∧ 𝑢 ∈ 𝑈)) ∧ (𝑠(+g‘𝐺)𝑢) ∈ 𝑇) → ( 0 (+g‘𝐺) 0 ) = 0 ) |
63 | 57, 62 | eqtrd 2656 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑠 ∈ 𝑆 ∧ 𝑢 ∈ 𝑈)) ∧ (𝑠(+g‘𝐺)𝑢) ∈ 𝑇) → (𝑠(+g‘𝐺)𝑢) = 0 ) |
64 | 63 | ex 450 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑠 ∈ 𝑆 ∧ 𝑢 ∈ 𝑈)) → ((𝑠(+g‘𝐺)𝑢) ∈ 𝑇 → (𝑠(+g‘𝐺)𝑢) = 0 )) |
65 | | eleq1 2689 |
. . . . . . . . . 10
⊢ (𝑥 = (𝑠(+g‘𝐺)𝑢) → (𝑥 ∈ 𝑇 ↔ (𝑠(+g‘𝐺)𝑢) ∈ 𝑇)) |
66 | | eqeq1 2626 |
. . . . . . . . . 10
⊢ (𝑥 = (𝑠(+g‘𝐺)𝑢) → (𝑥 = 0 ↔ (𝑠(+g‘𝐺)𝑢) = 0 )) |
67 | 65, 66 | imbi12d 334 |
. . . . . . . . 9
⊢ (𝑥 = (𝑠(+g‘𝐺)𝑢) → ((𝑥 ∈ 𝑇 → 𝑥 = 0 ) ↔ ((𝑠(+g‘𝐺)𝑢) ∈ 𝑇 → (𝑠(+g‘𝐺)𝑢) = 0 ))) |
68 | 64, 67 | syl5ibrcom 237 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑠 ∈ 𝑆 ∧ 𝑢 ∈ 𝑈)) → (𝑥 = (𝑠(+g‘𝐺)𝑢) → (𝑥 ∈ 𝑇 → 𝑥 = 0 ))) |
69 | 68 | rexlimdvva 3038 |
. . . . . . 7
⊢ (𝜑 → (∃𝑠 ∈ 𝑆 ∃𝑢 ∈ 𝑈 𝑥 = (𝑠(+g‘𝐺)𝑢) → (𝑥 ∈ 𝑇 → 𝑥 = 0 ))) |
70 | 6, 69 | sylbid 230 |
. . . . . 6
⊢ (𝜑 → (𝑥 ∈ (𝑆 ⊕ 𝑈) → (𝑥 ∈ 𝑇 → 𝑥 = 0 ))) |
71 | 70 | com23 86 |
. . . . 5
⊢ (𝜑 → (𝑥 ∈ 𝑇 → (𝑥 ∈ (𝑆 ⊕ 𝑈) → 𝑥 = 0 ))) |
72 | 71 | impd 447 |
. . . 4
⊢ (𝜑 → ((𝑥 ∈ 𝑇 ∧ 𝑥 ∈ (𝑆 ⊕ 𝑈)) → 𝑥 = 0 )) |
73 | | elin 3796 |
. . . 4
⊢ (𝑥 ∈ (𝑇 ∩ (𝑆 ⊕ 𝑈)) ↔ (𝑥 ∈ 𝑇 ∧ 𝑥 ∈ (𝑆 ⊕ 𝑈))) |
74 | | velsn 4193 |
. . . 4
⊢ (𝑥 ∈ { 0 } ↔ 𝑥 = 0 ) |
75 | 72, 73, 74 | 3imtr4g 285 |
. . 3
⊢ (𝜑 → (𝑥 ∈ (𝑇 ∩ (𝑆 ⊕ 𝑈)) → 𝑥 ∈ { 0 })) |
76 | 75 | ssrdv 3609 |
. 2
⊢ (𝜑 → (𝑇 ∩ (𝑆 ⊕ 𝑈)) ⊆ { 0 }) |
77 | 16 | subg0cl 17602 |
. . . . 5
⊢ (𝑇 ∈ (SubGrp‘𝐺) → 0 ∈ 𝑇) |
78 | 34, 77 | syl 17 |
. . . 4
⊢ (𝜑 → 0 ∈ 𝑇) |
79 | 4 | lsmub1 18071 |
. . . . . 6
⊢ ((𝑆 ∈ (SubGrp‘𝐺) ∧ 𝑈 ∈ (SubGrp‘𝐺)) → 𝑆 ⊆ (𝑆 ⊕ 𝑈)) |
80 | 1, 2, 79 | syl2anc 693 |
. . . . 5
⊢ (𝜑 → 𝑆 ⊆ (𝑆 ⊕ 𝑈)) |
81 | 16 | subg0cl 17602 |
. . . . . 6
⊢ (𝑆 ∈ (SubGrp‘𝐺) → 0 ∈ 𝑆) |
82 | 1, 81 | syl 17 |
. . . . 5
⊢ (𝜑 → 0 ∈ 𝑆) |
83 | 80, 82 | sseldd 3604 |
. . . 4
⊢ (𝜑 → 0 ∈ (𝑆 ⊕ 𝑈)) |
84 | 78, 83 | elind 3798 |
. . 3
⊢ (𝜑 → 0 ∈ (𝑇 ∩ (𝑆 ⊕ 𝑈))) |
85 | 84 | snssd 4340 |
. 2
⊢ (𝜑 → { 0 } ⊆ (𝑇 ∩ (𝑆 ⊕ 𝑈))) |
86 | 76, 85 | eqssd 3620 |
1
⊢ (𝜑 → (𝑇 ∩ (𝑆 ⊕ 𝑈)) = { 0 }) |