Step | Hyp | Ref
| Expression |
1 | | pj1eu.2 |
. . . . . . 7
⊢ (𝜑 → 𝑇 ∈ (SubGrp‘𝐺)) |
2 | | subgrcl 18548 |
. . . . . . 7
⊢ (𝑇 ∈ (SubGrp‘𝐺) → 𝐺 ∈ Grp) |
3 | 1, 2 | syl 17 |
. . . . . 6
⊢ (𝜑 → 𝐺 ∈ Grp) |
4 | | eqid 2737 |
. . . . . . . 8
⊢
(Base‘𝐺) =
(Base‘𝐺) |
5 | 4 | subgss 18544 |
. . . . . . 7
⊢ (𝑇 ∈ (SubGrp‘𝐺) → 𝑇 ⊆ (Base‘𝐺)) |
6 | 1, 5 | syl 17 |
. . . . . 6
⊢ (𝜑 → 𝑇 ⊆ (Base‘𝐺)) |
7 | | pj1eu.3 |
. . . . . . 7
⊢ (𝜑 → 𝑈 ∈ (SubGrp‘𝐺)) |
8 | 4 | subgss 18544 |
. . . . . . 7
⊢ (𝑈 ∈ (SubGrp‘𝐺) → 𝑈 ⊆ (Base‘𝐺)) |
9 | 7, 8 | syl 17 |
. . . . . 6
⊢ (𝜑 → 𝑈 ⊆ (Base‘𝐺)) |
10 | 3, 6, 9 | 3jca 1130 |
. . . . 5
⊢ (𝜑 → (𝐺 ∈ Grp ∧ 𝑇 ⊆ (Base‘𝐺) ∧ 𝑈 ⊆ (Base‘𝐺))) |
11 | | pj1eu.a |
. . . . . 6
⊢ + =
(+g‘𝐺) |
12 | | pj1eu.s |
. . . . . 6
⊢ ⊕ =
(LSSum‘𝐺) |
13 | | pj1f.p |
. . . . . 6
⊢ 𝑃 = (proj1‘𝐺) |
14 | 4, 11, 12, 13 | pj1val 19085 |
. . . . 5
⊢ (((𝐺 ∈ Grp ∧ 𝑇 ⊆ (Base‘𝐺) ∧ 𝑈 ⊆ (Base‘𝐺)) ∧ 𝑋 ∈ (𝑇 ⊕ 𝑈)) → ((𝑇𝑃𝑈)‘𝑋) = (℩𝑥 ∈ 𝑇 ∃𝑦 ∈ 𝑈 𝑋 = (𝑥 + 𝑦))) |
15 | 10, 14 | sylan 583 |
. . . 4
⊢ ((𝜑 ∧ 𝑋 ∈ (𝑇 ⊕ 𝑈)) → ((𝑇𝑃𝑈)‘𝑋) = (℩𝑥 ∈ 𝑇 ∃𝑦 ∈ 𝑈 𝑋 = (𝑥 + 𝑦))) |
16 | | pj1eu.o |
. . . . . 6
⊢ 0 =
(0g‘𝐺) |
17 | | pj1eu.z |
. . . . . 6
⊢ 𝑍 = (Cntz‘𝐺) |
18 | | pj1eu.4 |
. . . . . 6
⊢ (𝜑 → (𝑇 ∩ 𝑈) = { 0 }) |
19 | | pj1eu.5 |
. . . . . 6
⊢ (𝜑 → 𝑇 ⊆ (𝑍‘𝑈)) |
20 | 11, 12, 16, 17, 1, 7, 18, 19 | pj1eu 19086 |
. . . . 5
⊢ ((𝜑 ∧ 𝑋 ∈ (𝑇 ⊕ 𝑈)) → ∃!𝑥 ∈ 𝑇 ∃𝑦 ∈ 𝑈 𝑋 = (𝑥 + 𝑦)) |
21 | | riotacl2 7187 |
. . . . 5
⊢
(∃!𝑥 ∈
𝑇 ∃𝑦 ∈ 𝑈 𝑋 = (𝑥 + 𝑦) → (℩𝑥 ∈ 𝑇 ∃𝑦 ∈ 𝑈 𝑋 = (𝑥 + 𝑦)) ∈ {𝑥 ∈ 𝑇 ∣ ∃𝑦 ∈ 𝑈 𝑋 = (𝑥 + 𝑦)}) |
22 | 20, 21 | syl 17 |
. . . 4
⊢ ((𝜑 ∧ 𝑋 ∈ (𝑇 ⊕ 𝑈)) → (℩𝑥 ∈ 𝑇 ∃𝑦 ∈ 𝑈 𝑋 = (𝑥 + 𝑦)) ∈ {𝑥 ∈ 𝑇 ∣ ∃𝑦 ∈ 𝑈 𝑋 = (𝑥 + 𝑦)}) |
23 | 15, 22 | eqeltrd 2838 |
. . 3
⊢ ((𝜑 ∧ 𝑋 ∈ (𝑇 ⊕ 𝑈)) → ((𝑇𝑃𝑈)‘𝑋) ∈ {𝑥 ∈ 𝑇 ∣ ∃𝑦 ∈ 𝑈 𝑋 = (𝑥 + 𝑦)}) |
24 | | oveq1 7220 |
. . . . . . 7
⊢ (𝑥 = ((𝑇𝑃𝑈)‘𝑋) → (𝑥 + 𝑦) = (((𝑇𝑃𝑈)‘𝑋) + 𝑦)) |
25 | 24 | eqeq2d 2748 |
. . . . . 6
⊢ (𝑥 = ((𝑇𝑃𝑈)‘𝑋) → (𝑋 = (𝑥 + 𝑦) ↔ 𝑋 = (((𝑇𝑃𝑈)‘𝑋) + 𝑦))) |
26 | 25 | rexbidv 3216 |
. . . . 5
⊢ (𝑥 = ((𝑇𝑃𝑈)‘𝑋) → (∃𝑦 ∈ 𝑈 𝑋 = (𝑥 + 𝑦) ↔ ∃𝑦 ∈ 𝑈 𝑋 = (((𝑇𝑃𝑈)‘𝑋) + 𝑦))) |
27 | 26 | elrab 3602 |
. . . 4
⊢ (((𝑇𝑃𝑈)‘𝑋) ∈ {𝑥 ∈ 𝑇 ∣ ∃𝑦 ∈ 𝑈 𝑋 = (𝑥 + 𝑦)} ↔ (((𝑇𝑃𝑈)‘𝑋) ∈ 𝑇 ∧ ∃𝑦 ∈ 𝑈 𝑋 = (((𝑇𝑃𝑈)‘𝑋) + 𝑦))) |
28 | 27 | simprbi 500 |
. . 3
⊢ (((𝑇𝑃𝑈)‘𝑋) ∈ {𝑥 ∈ 𝑇 ∣ ∃𝑦 ∈ 𝑈 𝑋 = (𝑥 + 𝑦)} → ∃𝑦 ∈ 𝑈 𝑋 = (((𝑇𝑃𝑈)‘𝑋) + 𝑦)) |
29 | 23, 28 | syl 17 |
. 2
⊢ ((𝜑 ∧ 𝑋 ∈ (𝑇 ⊕ 𝑈)) → ∃𝑦 ∈ 𝑈 𝑋 = (((𝑇𝑃𝑈)‘𝑋) + 𝑦)) |
30 | | simprr 773 |
. . 3
⊢ (((𝜑 ∧ 𝑋 ∈ (𝑇 ⊕ 𝑈)) ∧ (𝑦 ∈ 𝑈 ∧ 𝑋 = (((𝑇𝑃𝑈)‘𝑋) + 𝑦))) → 𝑋 = (((𝑇𝑃𝑈)‘𝑋) + 𝑦)) |
31 | 3 | ad2antrr 726 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑋 ∈ (𝑇 ⊕ 𝑈)) ∧ (𝑦 ∈ 𝑈 ∧ 𝑋 = (((𝑇𝑃𝑈)‘𝑋) + 𝑦))) → 𝐺 ∈ Grp) |
32 | 9 | ad2antrr 726 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑋 ∈ (𝑇 ⊕ 𝑈)) ∧ (𝑦 ∈ 𝑈 ∧ 𝑋 = (((𝑇𝑃𝑈)‘𝑋) + 𝑦))) → 𝑈 ⊆ (Base‘𝐺)) |
33 | 6 | ad2antrr 726 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑋 ∈ (𝑇 ⊕ 𝑈)) ∧ (𝑦 ∈ 𝑈 ∧ 𝑋 = (((𝑇𝑃𝑈)‘𝑋) + 𝑦))) → 𝑇 ⊆ (Base‘𝐺)) |
34 | | simplr 769 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑋 ∈ (𝑇 ⊕ 𝑈)) ∧ (𝑦 ∈ 𝑈 ∧ 𝑋 = (((𝑇𝑃𝑈)‘𝑋) + 𝑦))) → 𝑋 ∈ (𝑇 ⊕ 𝑈)) |
35 | 12, 17 | lsmcom2 19044 |
. . . . . . . . 9
⊢ ((𝑇 ∈ (SubGrp‘𝐺) ∧ 𝑈 ∈ (SubGrp‘𝐺) ∧ 𝑇 ⊆ (𝑍‘𝑈)) → (𝑇 ⊕ 𝑈) = (𝑈 ⊕ 𝑇)) |
36 | 1, 7, 19, 35 | syl3anc 1373 |
. . . . . . . 8
⊢ (𝜑 → (𝑇 ⊕ 𝑈) = (𝑈 ⊕ 𝑇)) |
37 | 36 | ad2antrr 726 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑋 ∈ (𝑇 ⊕ 𝑈)) ∧ (𝑦 ∈ 𝑈 ∧ 𝑋 = (((𝑇𝑃𝑈)‘𝑋) + 𝑦))) → (𝑇 ⊕ 𝑈) = (𝑈 ⊕ 𝑇)) |
38 | 34, 37 | eleqtrd 2840 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑋 ∈ (𝑇 ⊕ 𝑈)) ∧ (𝑦 ∈ 𝑈 ∧ 𝑋 = (((𝑇𝑃𝑈)‘𝑋) + 𝑦))) → 𝑋 ∈ (𝑈 ⊕ 𝑇)) |
39 | 4, 11, 12, 13 | pj1val 19085 |
. . . . . 6
⊢ (((𝐺 ∈ Grp ∧ 𝑈 ⊆ (Base‘𝐺) ∧ 𝑇 ⊆ (Base‘𝐺)) ∧ 𝑋 ∈ (𝑈 ⊕ 𝑇)) → ((𝑈𝑃𝑇)‘𝑋) = (℩𝑢 ∈ 𝑈 ∃𝑣 ∈ 𝑇 𝑋 = (𝑢 + 𝑣))) |
40 | 31, 32, 33, 38, 39 | syl31anc 1375 |
. . . . 5
⊢ (((𝜑 ∧ 𝑋 ∈ (𝑇 ⊕ 𝑈)) ∧ (𝑦 ∈ 𝑈 ∧ 𝑋 = (((𝑇𝑃𝑈)‘𝑋) + 𝑦))) → ((𝑈𝑃𝑇)‘𝑋) = (℩𝑢 ∈ 𝑈 ∃𝑣 ∈ 𝑇 𝑋 = (𝑢 + 𝑣))) |
41 | 11, 12, 16, 17, 1, 7, 18, 19, 13 | pj1f 19087 |
. . . . . . . . 9
⊢ (𝜑 → (𝑇𝑃𝑈):(𝑇 ⊕ 𝑈)⟶𝑇) |
42 | 41 | ad2antrr 726 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑋 ∈ (𝑇 ⊕ 𝑈)) ∧ (𝑦 ∈ 𝑈 ∧ 𝑋 = (((𝑇𝑃𝑈)‘𝑋) + 𝑦))) → (𝑇𝑃𝑈):(𝑇 ⊕ 𝑈)⟶𝑇) |
43 | 42, 34 | ffvelrnd 6905 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑋 ∈ (𝑇 ⊕ 𝑈)) ∧ (𝑦 ∈ 𝑈 ∧ 𝑋 = (((𝑇𝑃𝑈)‘𝑋) + 𝑦))) → ((𝑇𝑃𝑈)‘𝑋) ∈ 𝑇) |
44 | 19 | ad2antrr 726 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑋 ∈ (𝑇 ⊕ 𝑈)) ∧ (𝑦 ∈ 𝑈 ∧ 𝑋 = (((𝑇𝑃𝑈)‘𝑋) + 𝑦))) → 𝑇 ⊆ (𝑍‘𝑈)) |
45 | 44, 43 | sseldd 3902 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑋 ∈ (𝑇 ⊕ 𝑈)) ∧ (𝑦 ∈ 𝑈 ∧ 𝑋 = (((𝑇𝑃𝑈)‘𝑋) + 𝑦))) → ((𝑇𝑃𝑈)‘𝑋) ∈ (𝑍‘𝑈)) |
46 | | simprl 771 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑋 ∈ (𝑇 ⊕ 𝑈)) ∧ (𝑦 ∈ 𝑈 ∧ 𝑋 = (((𝑇𝑃𝑈)‘𝑋) + 𝑦))) → 𝑦 ∈ 𝑈) |
47 | 11, 17 | cntzi 18723 |
. . . . . . . . 9
⊢ ((((𝑇𝑃𝑈)‘𝑋) ∈ (𝑍‘𝑈) ∧ 𝑦 ∈ 𝑈) → (((𝑇𝑃𝑈)‘𝑋) + 𝑦) = (𝑦 + ((𝑇𝑃𝑈)‘𝑋))) |
48 | 45, 46, 47 | syl2anc 587 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑋 ∈ (𝑇 ⊕ 𝑈)) ∧ (𝑦 ∈ 𝑈 ∧ 𝑋 = (((𝑇𝑃𝑈)‘𝑋) + 𝑦))) → (((𝑇𝑃𝑈)‘𝑋) + 𝑦) = (𝑦 + ((𝑇𝑃𝑈)‘𝑋))) |
49 | 30, 48 | eqtrd 2777 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑋 ∈ (𝑇 ⊕ 𝑈)) ∧ (𝑦 ∈ 𝑈 ∧ 𝑋 = (((𝑇𝑃𝑈)‘𝑋) + 𝑦))) → 𝑋 = (𝑦 + ((𝑇𝑃𝑈)‘𝑋))) |
50 | | oveq2 7221 |
. . . . . . . 8
⊢ (𝑣 = ((𝑇𝑃𝑈)‘𝑋) → (𝑦 + 𝑣) = (𝑦 + ((𝑇𝑃𝑈)‘𝑋))) |
51 | 50 | rspceeqv 3552 |
. . . . . . 7
⊢ ((((𝑇𝑃𝑈)‘𝑋) ∈ 𝑇 ∧ 𝑋 = (𝑦 + ((𝑇𝑃𝑈)‘𝑋))) → ∃𝑣 ∈ 𝑇 𝑋 = (𝑦 + 𝑣)) |
52 | 43, 49, 51 | syl2anc 587 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑋 ∈ (𝑇 ⊕ 𝑈)) ∧ (𝑦 ∈ 𝑈 ∧ 𝑋 = (((𝑇𝑃𝑈)‘𝑋) + 𝑦))) → ∃𝑣 ∈ 𝑇 𝑋 = (𝑦 + 𝑣)) |
53 | | simpll 767 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑋 ∈ (𝑇 ⊕ 𝑈)) ∧ (𝑦 ∈ 𝑈 ∧ 𝑋 = (((𝑇𝑃𝑈)‘𝑋) + 𝑦))) → 𝜑) |
54 | | incom 4115 |
. . . . . . . . . 10
⊢ (𝑈 ∩ 𝑇) = (𝑇 ∩ 𝑈) |
55 | 54, 18 | syl5eq 2790 |
. . . . . . . . 9
⊢ (𝜑 → (𝑈 ∩ 𝑇) = { 0 }) |
56 | 17, 1, 7, 19 | cntzrecd 19068 |
. . . . . . . . 9
⊢ (𝜑 → 𝑈 ⊆ (𝑍‘𝑇)) |
57 | 11, 12, 16, 17, 7, 1, 55, 56 | pj1eu 19086 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑋 ∈ (𝑈 ⊕ 𝑇)) → ∃!𝑢 ∈ 𝑈 ∃𝑣 ∈ 𝑇 𝑋 = (𝑢 + 𝑣)) |
58 | 53, 38, 57 | syl2anc 587 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑋 ∈ (𝑇 ⊕ 𝑈)) ∧ (𝑦 ∈ 𝑈 ∧ 𝑋 = (((𝑇𝑃𝑈)‘𝑋) + 𝑦))) → ∃!𝑢 ∈ 𝑈 ∃𝑣 ∈ 𝑇 𝑋 = (𝑢 + 𝑣)) |
59 | | oveq1 7220 |
. . . . . . . . . 10
⊢ (𝑢 = 𝑦 → (𝑢 + 𝑣) = (𝑦 + 𝑣)) |
60 | 59 | eqeq2d 2748 |
. . . . . . . . 9
⊢ (𝑢 = 𝑦 → (𝑋 = (𝑢 + 𝑣) ↔ 𝑋 = (𝑦 + 𝑣))) |
61 | 60 | rexbidv 3216 |
. . . . . . . 8
⊢ (𝑢 = 𝑦 → (∃𝑣 ∈ 𝑇 𝑋 = (𝑢 + 𝑣) ↔ ∃𝑣 ∈ 𝑇 𝑋 = (𝑦 + 𝑣))) |
62 | 61 | riota2 7196 |
. . . . . . 7
⊢ ((𝑦 ∈ 𝑈 ∧ ∃!𝑢 ∈ 𝑈 ∃𝑣 ∈ 𝑇 𝑋 = (𝑢 + 𝑣)) → (∃𝑣 ∈ 𝑇 𝑋 = (𝑦 + 𝑣) ↔ (℩𝑢 ∈ 𝑈 ∃𝑣 ∈ 𝑇 𝑋 = (𝑢 + 𝑣)) = 𝑦)) |
63 | 46, 58, 62 | syl2anc 587 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑋 ∈ (𝑇 ⊕ 𝑈)) ∧ (𝑦 ∈ 𝑈 ∧ 𝑋 = (((𝑇𝑃𝑈)‘𝑋) + 𝑦))) → (∃𝑣 ∈ 𝑇 𝑋 = (𝑦 + 𝑣) ↔ (℩𝑢 ∈ 𝑈 ∃𝑣 ∈ 𝑇 𝑋 = (𝑢 + 𝑣)) = 𝑦)) |
64 | 52, 63 | mpbid 235 |
. . . . 5
⊢ (((𝜑 ∧ 𝑋 ∈ (𝑇 ⊕ 𝑈)) ∧ (𝑦 ∈ 𝑈 ∧ 𝑋 = (((𝑇𝑃𝑈)‘𝑋) + 𝑦))) → (℩𝑢 ∈ 𝑈 ∃𝑣 ∈ 𝑇 𝑋 = (𝑢 + 𝑣)) = 𝑦) |
65 | 40, 64 | eqtrd 2777 |
. . . 4
⊢ (((𝜑 ∧ 𝑋 ∈ (𝑇 ⊕ 𝑈)) ∧ (𝑦 ∈ 𝑈 ∧ 𝑋 = (((𝑇𝑃𝑈)‘𝑋) + 𝑦))) → ((𝑈𝑃𝑇)‘𝑋) = 𝑦) |
66 | 65 | oveq2d 7229 |
. . 3
⊢ (((𝜑 ∧ 𝑋 ∈ (𝑇 ⊕ 𝑈)) ∧ (𝑦 ∈ 𝑈 ∧ 𝑋 = (((𝑇𝑃𝑈)‘𝑋) + 𝑦))) → (((𝑇𝑃𝑈)‘𝑋) + ((𝑈𝑃𝑇)‘𝑋)) = (((𝑇𝑃𝑈)‘𝑋) + 𝑦)) |
67 | 30, 66 | eqtr4d 2780 |
. 2
⊢ (((𝜑 ∧ 𝑋 ∈ (𝑇 ⊕ 𝑈)) ∧ (𝑦 ∈ 𝑈 ∧ 𝑋 = (((𝑇𝑃𝑈)‘𝑋) + 𝑦))) → 𝑋 = (((𝑇𝑃𝑈)‘𝑋) + ((𝑈𝑃𝑇)‘𝑋))) |
68 | 29, 67 | rexlimddv 3210 |
1
⊢ ((𝜑 ∧ 𝑋 ∈ (𝑇 ⊕ 𝑈)) → 𝑋 = (((𝑇𝑃𝑈)‘𝑋) + ((𝑈𝑃𝑇)‘𝑋))) |