Step | Hyp | Ref
| Expression |
1 | | lsmcntz.s |
. . . . . . 7
⊢ (𝜑 → 𝑆 ∈ (SubGrp‘𝐺)) |
2 | | lsmcntz.u |
. . . . . . 7
⊢ (𝜑 → 𝑈 ∈ (SubGrp‘𝐺)) |
3 | | eqid 2738 |
. . . . . . . 8
⊢
(+g‘𝐺) = (+g‘𝐺) |
4 | | lsmcntz.p |
. . . . . . . 8
⊢ ⊕ =
(LSSum‘𝐺) |
5 | 3, 4 | lsmelval 19243 |
. . . . . . 7
⊢ ((𝑆 ∈ (SubGrp‘𝐺) ∧ 𝑈 ∈ (SubGrp‘𝐺)) → (𝑥 ∈ (𝑆 ⊕ 𝑈) ↔ ∃𝑠 ∈ 𝑆 ∃𝑢 ∈ 𝑈 𝑥 = (𝑠(+g‘𝐺)𝑢))) |
6 | 1, 2, 5 | syl2anc 584 |
. . . . . 6
⊢ (𝜑 → (𝑥 ∈ (𝑆 ⊕ 𝑈) ↔ ∃𝑠 ∈ 𝑆 ∃𝑢 ∈ 𝑈 𝑥 = (𝑠(+g‘𝐺)𝑢))) |
7 | | simplrl 774 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑠 ∈ 𝑆 ∧ 𝑢 ∈ 𝑈)) ∧ (𝑠(+g‘𝐺)𝑢) ∈ 𝑇) → 𝑠 ∈ 𝑆) |
8 | | subgrcl 18749 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑆 ∈ (SubGrp‘𝐺) → 𝐺 ∈ Grp) |
9 | 1, 8 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝜑 → 𝐺 ∈ Grp) |
10 | 9 | ad2antrr 723 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝜑 ∧ (𝑠 ∈ 𝑆 ∧ 𝑢 ∈ 𝑈)) ∧ (𝑠(+g‘𝐺)𝑢) ∈ 𝑇) → 𝐺 ∈ Grp) |
11 | 1 | ad2antrr 723 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝜑 ∧ (𝑠 ∈ 𝑆 ∧ 𝑢 ∈ 𝑈)) ∧ (𝑠(+g‘𝐺)𝑢) ∈ 𝑇) → 𝑆 ∈ (SubGrp‘𝐺)) |
12 | | eqid 2738 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
(Base‘𝐺) =
(Base‘𝐺) |
13 | 12 | subgss 18745 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑆 ∈ (SubGrp‘𝐺) → 𝑆 ⊆ (Base‘𝐺)) |
14 | 11, 13 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝜑 ∧ (𝑠 ∈ 𝑆 ∧ 𝑢 ∈ 𝑈)) ∧ (𝑠(+g‘𝐺)𝑢) ∈ 𝑇) → 𝑆 ⊆ (Base‘𝐺)) |
15 | 14, 7 | sseldd 3923 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝜑 ∧ (𝑠 ∈ 𝑆 ∧ 𝑢 ∈ 𝑈)) ∧ (𝑠(+g‘𝐺)𝑢) ∈ 𝑇) → 𝑠 ∈ (Base‘𝐺)) |
16 | | lsmdisj.o |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ 0 =
(0g‘𝐺) |
17 | | eqid 2738 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
(invg‘𝐺) = (invg‘𝐺) |
18 | 12, 3, 16, 17 | grplinv 18617 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝐺 ∈ Grp ∧ 𝑠 ∈ (Base‘𝐺)) →
(((invg‘𝐺)‘𝑠)(+g‘𝐺)𝑠) = 0 ) |
19 | 10, 15, 18 | syl2anc 584 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝜑 ∧ (𝑠 ∈ 𝑆 ∧ 𝑢 ∈ 𝑈)) ∧ (𝑠(+g‘𝐺)𝑢) ∈ 𝑇) → (((invg‘𝐺)‘𝑠)(+g‘𝐺)𝑠) = 0 ) |
20 | 19 | oveq1d 7284 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ (𝑠 ∈ 𝑆 ∧ 𝑢 ∈ 𝑈)) ∧ (𝑠(+g‘𝐺)𝑢) ∈ 𝑇) → ((((invg‘𝐺)‘𝑠)(+g‘𝐺)𝑠)(+g‘𝐺)𝑢) = ( 0 (+g‘𝐺)𝑢)) |
21 | 17 | subginvcl 18753 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑆 ∈ (SubGrp‘𝐺) ∧ 𝑠 ∈ 𝑆) → ((invg‘𝐺)‘𝑠) ∈ 𝑆) |
22 | 11, 7, 21 | syl2anc 584 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝜑 ∧ (𝑠 ∈ 𝑆 ∧ 𝑢 ∈ 𝑈)) ∧ (𝑠(+g‘𝐺)𝑢) ∈ 𝑇) → ((invg‘𝐺)‘𝑠) ∈ 𝑆) |
23 | 14, 22 | sseldd 3923 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝜑 ∧ (𝑠 ∈ 𝑆 ∧ 𝑢 ∈ 𝑈)) ∧ (𝑠(+g‘𝐺)𝑢) ∈ 𝑇) → ((invg‘𝐺)‘𝑠) ∈ (Base‘𝐺)) |
24 | 2 | ad2antrr 723 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝜑 ∧ (𝑠 ∈ 𝑆 ∧ 𝑢 ∈ 𝑈)) ∧ (𝑠(+g‘𝐺)𝑢) ∈ 𝑇) → 𝑈 ∈ (SubGrp‘𝐺)) |
25 | 12 | subgss 18745 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑈 ∈ (SubGrp‘𝐺) → 𝑈 ⊆ (Base‘𝐺)) |
26 | 24, 25 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝜑 ∧ (𝑠 ∈ 𝑆 ∧ 𝑢 ∈ 𝑈)) ∧ (𝑠(+g‘𝐺)𝑢) ∈ 𝑇) → 𝑈 ⊆ (Base‘𝐺)) |
27 | | simplrr 775 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝜑 ∧ (𝑠 ∈ 𝑆 ∧ 𝑢 ∈ 𝑈)) ∧ (𝑠(+g‘𝐺)𝑢) ∈ 𝑇) → 𝑢 ∈ 𝑈) |
28 | 26, 27 | sseldd 3923 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝜑 ∧ (𝑠 ∈ 𝑆 ∧ 𝑢 ∈ 𝑈)) ∧ (𝑠(+g‘𝐺)𝑢) ∈ 𝑇) → 𝑢 ∈ (Base‘𝐺)) |
29 | 12, 3 | grpass 18575 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝐺 ∈ Grp ∧
(((invg‘𝐺)‘𝑠) ∈ (Base‘𝐺) ∧ 𝑠 ∈ (Base‘𝐺) ∧ 𝑢 ∈ (Base‘𝐺))) → ((((invg‘𝐺)‘𝑠)(+g‘𝐺)𝑠)(+g‘𝐺)𝑢) = (((invg‘𝐺)‘𝑠)(+g‘𝐺)(𝑠(+g‘𝐺)𝑢))) |
30 | 10, 23, 15, 28, 29 | syl13anc 1371 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ (𝑠 ∈ 𝑆 ∧ 𝑢 ∈ 𝑈)) ∧ (𝑠(+g‘𝐺)𝑢) ∈ 𝑇) → ((((invg‘𝐺)‘𝑠)(+g‘𝐺)𝑠)(+g‘𝐺)𝑢) = (((invg‘𝐺)‘𝑠)(+g‘𝐺)(𝑠(+g‘𝐺)𝑢))) |
31 | 12, 3, 16 | grplid 18598 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝐺 ∈ Grp ∧ 𝑢 ∈ (Base‘𝐺)) → ( 0 (+g‘𝐺)𝑢) = 𝑢) |
32 | 10, 28, 31 | syl2anc 584 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ (𝑠 ∈ 𝑆 ∧ 𝑢 ∈ 𝑈)) ∧ (𝑠(+g‘𝐺)𝑢) ∈ 𝑇) → ( 0 (+g‘𝐺)𝑢) = 𝑢) |
33 | 20, 30, 32 | 3eqtr3d 2786 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ (𝑠 ∈ 𝑆 ∧ 𝑢 ∈ 𝑈)) ∧ (𝑠(+g‘𝐺)𝑢) ∈ 𝑇) → (((invg‘𝐺)‘𝑠)(+g‘𝐺)(𝑠(+g‘𝐺)𝑢)) = 𝑢) |
34 | | lsmcntz.t |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜑 → 𝑇 ∈ (SubGrp‘𝐺)) |
35 | 34 | ad2antrr 723 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ (𝑠 ∈ 𝑆 ∧ 𝑢 ∈ 𝑈)) ∧ (𝑠(+g‘𝐺)𝑢) ∈ 𝑇) → 𝑇 ∈ (SubGrp‘𝐺)) |
36 | | simpr 485 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ (𝑠 ∈ 𝑆 ∧ 𝑢 ∈ 𝑈)) ∧ (𝑠(+g‘𝐺)𝑢) ∈ 𝑇) → (𝑠(+g‘𝐺)𝑢) ∈ 𝑇) |
37 | 3, 4 | lsmelvali 19244 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝑆 ∈ (SubGrp‘𝐺) ∧ 𝑇 ∈ (SubGrp‘𝐺)) ∧ (((invg‘𝐺)‘𝑠) ∈ 𝑆 ∧ (𝑠(+g‘𝐺)𝑢) ∈ 𝑇)) → (((invg‘𝐺)‘𝑠)(+g‘𝐺)(𝑠(+g‘𝐺)𝑢)) ∈ (𝑆 ⊕ 𝑇)) |
38 | 11, 35, 22, 36, 37 | syl22anc 836 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ (𝑠 ∈ 𝑆 ∧ 𝑢 ∈ 𝑈)) ∧ (𝑠(+g‘𝐺)𝑢) ∈ 𝑇) → (((invg‘𝐺)‘𝑠)(+g‘𝐺)(𝑠(+g‘𝐺)𝑢)) ∈ (𝑆 ⊕ 𝑇)) |
39 | 33, 38 | eqeltrrd 2840 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ (𝑠 ∈ 𝑆 ∧ 𝑢 ∈ 𝑈)) ∧ (𝑠(+g‘𝐺)𝑢) ∈ 𝑇) → 𝑢 ∈ (𝑆 ⊕ 𝑇)) |
40 | 39, 27 | elind 4129 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ (𝑠 ∈ 𝑆 ∧ 𝑢 ∈ 𝑈)) ∧ (𝑠(+g‘𝐺)𝑢) ∈ 𝑇) → 𝑢 ∈ ((𝑆 ⊕ 𝑇) ∩ 𝑈)) |
41 | | lsmdisj.i |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → ((𝑆 ⊕ 𝑇) ∩ 𝑈) = { 0 }) |
42 | 41 | ad2antrr 723 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ (𝑠 ∈ 𝑆 ∧ 𝑢 ∈ 𝑈)) ∧ (𝑠(+g‘𝐺)𝑢) ∈ 𝑇) → ((𝑆 ⊕ 𝑇) ∩ 𝑈) = { 0 }) |
43 | 40, 42 | eleqtrd 2841 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ (𝑠 ∈ 𝑆 ∧ 𝑢 ∈ 𝑈)) ∧ (𝑠(+g‘𝐺)𝑢) ∈ 𝑇) → 𝑢 ∈ { 0 }) |
44 | | elsni 4580 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑢 ∈ { 0 } → 𝑢 = 0 ) |
45 | 43, 44 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ (𝑠 ∈ 𝑆 ∧ 𝑢 ∈ 𝑈)) ∧ (𝑠(+g‘𝐺)𝑢) ∈ 𝑇) → 𝑢 = 0 ) |
46 | 45 | oveq2d 7285 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑠 ∈ 𝑆 ∧ 𝑢 ∈ 𝑈)) ∧ (𝑠(+g‘𝐺)𝑢) ∈ 𝑇) → (𝑠(+g‘𝐺)𝑢) = (𝑠(+g‘𝐺) 0 )) |
47 | 12, 3, 16 | grprid 18599 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐺 ∈ Grp ∧ 𝑠 ∈ (Base‘𝐺)) → (𝑠(+g‘𝐺) 0 ) = 𝑠) |
48 | 10, 15, 47 | syl2anc 584 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑠 ∈ 𝑆 ∧ 𝑢 ∈ 𝑈)) ∧ (𝑠(+g‘𝐺)𝑢) ∈ 𝑇) → (𝑠(+g‘𝐺) 0 ) = 𝑠) |
49 | 46, 48 | eqtrd 2778 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑠 ∈ 𝑆 ∧ 𝑢 ∈ 𝑈)) ∧ (𝑠(+g‘𝐺)𝑢) ∈ 𝑇) → (𝑠(+g‘𝐺)𝑢) = 𝑠) |
50 | 49, 36 | eqeltrrd 2840 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑠 ∈ 𝑆 ∧ 𝑢 ∈ 𝑈)) ∧ (𝑠(+g‘𝐺)𝑢) ∈ 𝑇) → 𝑠 ∈ 𝑇) |
51 | 7, 50 | elind 4129 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑠 ∈ 𝑆 ∧ 𝑢 ∈ 𝑈)) ∧ (𝑠(+g‘𝐺)𝑢) ∈ 𝑇) → 𝑠 ∈ (𝑆 ∩ 𝑇)) |
52 | | lsmdisj2.i |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑆 ∩ 𝑇) = { 0 }) |
53 | 52 | ad2antrr 723 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑠 ∈ 𝑆 ∧ 𝑢 ∈ 𝑈)) ∧ (𝑠(+g‘𝐺)𝑢) ∈ 𝑇) → (𝑆 ∩ 𝑇) = { 0 }) |
54 | 51, 53 | eleqtrd 2841 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑠 ∈ 𝑆 ∧ 𝑢 ∈ 𝑈)) ∧ (𝑠(+g‘𝐺)𝑢) ∈ 𝑇) → 𝑠 ∈ { 0 }) |
55 | | elsni 4580 |
. . . . . . . . . . . 12
⊢ (𝑠 ∈ { 0 } → 𝑠 = 0 ) |
56 | 54, 55 | syl 17 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑠 ∈ 𝑆 ∧ 𝑢 ∈ 𝑈)) ∧ (𝑠(+g‘𝐺)𝑢) ∈ 𝑇) → 𝑠 = 0 ) |
57 | 56, 45 | oveq12d 7287 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑠 ∈ 𝑆 ∧ 𝑢 ∈ 𝑈)) ∧ (𝑠(+g‘𝐺)𝑢) ∈ 𝑇) → (𝑠(+g‘𝐺)𝑢) = ( 0 (+g‘𝐺) 0 )) |
58 | 12, 16 | grpidcl 18596 |
. . . . . . . . . . . 12
⊢ (𝐺 ∈ Grp → 0 ∈
(Base‘𝐺)) |
59 | 12, 3, 16 | grplid 18598 |
. . . . . . . . . . . 12
⊢ ((𝐺 ∈ Grp ∧ 0 ∈
(Base‘𝐺)) → (
0
(+g‘𝐺)
0 ) =
0
) |
60 | 9, 58, 59 | syl2anc2 585 |
. . . . . . . . . . 11
⊢ (𝜑 → ( 0 (+g‘𝐺) 0 ) = 0 ) |
61 | 60 | ad2antrr 723 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑠 ∈ 𝑆 ∧ 𝑢 ∈ 𝑈)) ∧ (𝑠(+g‘𝐺)𝑢) ∈ 𝑇) → ( 0 (+g‘𝐺) 0 ) = 0 ) |
62 | 57, 61 | eqtrd 2778 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑠 ∈ 𝑆 ∧ 𝑢 ∈ 𝑈)) ∧ (𝑠(+g‘𝐺)𝑢) ∈ 𝑇) → (𝑠(+g‘𝐺)𝑢) = 0 ) |
63 | 62 | ex 413 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑠 ∈ 𝑆 ∧ 𝑢 ∈ 𝑈)) → ((𝑠(+g‘𝐺)𝑢) ∈ 𝑇 → (𝑠(+g‘𝐺)𝑢) = 0 )) |
64 | | eleq1 2826 |
. . . . . . . . 9
⊢ (𝑥 = (𝑠(+g‘𝐺)𝑢) → (𝑥 ∈ 𝑇 ↔ (𝑠(+g‘𝐺)𝑢) ∈ 𝑇)) |
65 | | eqeq1 2742 |
. . . . . . . . 9
⊢ (𝑥 = (𝑠(+g‘𝐺)𝑢) → (𝑥 = 0 ↔ (𝑠(+g‘𝐺)𝑢) = 0 )) |
66 | 64, 65 | imbi12d 345 |
. . . . . . . 8
⊢ (𝑥 = (𝑠(+g‘𝐺)𝑢) → ((𝑥 ∈ 𝑇 → 𝑥 = 0 ) ↔ ((𝑠(+g‘𝐺)𝑢) ∈ 𝑇 → (𝑠(+g‘𝐺)𝑢) = 0 ))) |
67 | 63, 66 | syl5ibrcom 246 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑠 ∈ 𝑆 ∧ 𝑢 ∈ 𝑈)) → (𝑥 = (𝑠(+g‘𝐺)𝑢) → (𝑥 ∈ 𝑇 → 𝑥 = 0 ))) |
68 | 67 | rexlimdvva 3222 |
. . . . . 6
⊢ (𝜑 → (∃𝑠 ∈ 𝑆 ∃𝑢 ∈ 𝑈 𝑥 = (𝑠(+g‘𝐺)𝑢) → (𝑥 ∈ 𝑇 → 𝑥 = 0 ))) |
69 | 6, 68 | sylbid 239 |
. . . . 5
⊢ (𝜑 → (𝑥 ∈ (𝑆 ⊕ 𝑈) → (𝑥 ∈ 𝑇 → 𝑥 = 0 ))) |
70 | 69 | impcomd 412 |
. . . 4
⊢ (𝜑 → ((𝑥 ∈ 𝑇 ∧ 𝑥 ∈ (𝑆 ⊕ 𝑈)) → 𝑥 = 0 )) |
71 | | elin 3904 |
. . . 4
⊢ (𝑥 ∈ (𝑇 ∩ (𝑆 ⊕ 𝑈)) ↔ (𝑥 ∈ 𝑇 ∧ 𝑥 ∈ (𝑆 ⊕ 𝑈))) |
72 | | velsn 4579 |
. . . 4
⊢ (𝑥 ∈ { 0 } ↔ 𝑥 = 0 ) |
73 | 70, 71, 72 | 3imtr4g 296 |
. . 3
⊢ (𝜑 → (𝑥 ∈ (𝑇 ∩ (𝑆 ⊕ 𝑈)) → 𝑥 ∈ { 0 })) |
74 | 73 | ssrdv 3928 |
. 2
⊢ (𝜑 → (𝑇 ∩ (𝑆 ⊕ 𝑈)) ⊆ { 0 }) |
75 | 16 | subg0cl 18752 |
. . . . 5
⊢ (𝑇 ∈ (SubGrp‘𝐺) → 0 ∈ 𝑇) |
76 | 34, 75 | syl 17 |
. . . 4
⊢ (𝜑 → 0 ∈ 𝑇) |
77 | 4 | lsmub1 19251 |
. . . . . 6
⊢ ((𝑆 ∈ (SubGrp‘𝐺) ∧ 𝑈 ∈ (SubGrp‘𝐺)) → 𝑆 ⊆ (𝑆 ⊕ 𝑈)) |
78 | 1, 2, 77 | syl2anc 584 |
. . . . 5
⊢ (𝜑 → 𝑆 ⊆ (𝑆 ⊕ 𝑈)) |
79 | 16 | subg0cl 18752 |
. . . . . 6
⊢ (𝑆 ∈ (SubGrp‘𝐺) → 0 ∈ 𝑆) |
80 | 1, 79 | syl 17 |
. . . . 5
⊢ (𝜑 → 0 ∈ 𝑆) |
81 | 78, 80 | sseldd 3923 |
. . . 4
⊢ (𝜑 → 0 ∈ (𝑆 ⊕ 𝑈)) |
82 | 76, 81 | elind 4129 |
. . 3
⊢ (𝜑 → 0 ∈ (𝑇 ∩ (𝑆 ⊕ 𝑈))) |
83 | 82 | snssd 4744 |
. 2
⊢ (𝜑 → { 0 } ⊆ (𝑇 ∩ (𝑆 ⊕ 𝑈))) |
84 | 74, 83 | eqssd 3939 |
1
⊢ (𝜑 → (𝑇 ∩ (𝑆 ⊕ 𝑈)) = { 0 }) |