| Step | Hyp | Ref
| Expression |
| 1 | | pj1eu.2 |
. . . 4
⊢ (𝜑 → 𝑇 ∈ (SubGrp‘𝐺)) |
| 2 | | pj1eu.3 |
. . . 4
⊢ (𝜑 → 𝑈 ∈ (SubGrp‘𝐺)) |
| 3 | | pj1eu.a |
. . . . 5
⊢ + =
(+g‘𝐺) |
| 4 | | pj1eu.s |
. . . . 5
⊢ ⊕ =
(LSSum‘𝐺) |
| 5 | 3, 4 | lsmelval 19667 |
. . . 4
⊢ ((𝑇 ∈ (SubGrp‘𝐺) ∧ 𝑈 ∈ (SubGrp‘𝐺)) → (𝑋 ∈ (𝑇 ⊕ 𝑈) ↔ ∃𝑥 ∈ 𝑇 ∃𝑦 ∈ 𝑈 𝑋 = (𝑥 + 𝑦))) |
| 6 | 1, 2, 5 | syl2anc 584 |
. . 3
⊢ (𝜑 → (𝑋 ∈ (𝑇 ⊕ 𝑈) ↔ ∃𝑥 ∈ 𝑇 ∃𝑦 ∈ 𝑈 𝑋 = (𝑥 + 𝑦))) |
| 7 | 6 | biimpa 476 |
. 2
⊢ ((𝜑 ∧ 𝑋 ∈ (𝑇 ⊕ 𝑈)) → ∃𝑥 ∈ 𝑇 ∃𝑦 ∈ 𝑈 𝑋 = (𝑥 + 𝑦)) |
| 8 | | reeanv 3229 |
. . . . 5
⊢
(∃𝑦 ∈
𝑈 ∃𝑣 ∈ 𝑈 (𝑋 = (𝑥 + 𝑦) ∧ 𝑋 = (𝑢 + 𝑣)) ↔ (∃𝑦 ∈ 𝑈 𝑋 = (𝑥 + 𝑦) ∧ ∃𝑣 ∈ 𝑈 𝑋 = (𝑢 + 𝑣))) |
| 9 | | eqtr2 2761 |
. . . . . . 7
⊢ ((𝑋 = (𝑥 + 𝑦) ∧ 𝑋 = (𝑢 + 𝑣)) → (𝑥 + 𝑦) = (𝑢 + 𝑣)) |
| 10 | | pj1eu.o |
. . . . . . . . 9
⊢ 0 =
(0g‘𝐺) |
| 11 | | pj1eu.z |
. . . . . . . . 9
⊢ 𝑍 = (Cntz‘𝐺) |
| 12 | 1 | ad2antrr 726 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑥 ∈ 𝑇 ∧ 𝑢 ∈ 𝑇)) ∧ (𝑦 ∈ 𝑈 ∧ 𝑣 ∈ 𝑈)) → 𝑇 ∈ (SubGrp‘𝐺)) |
| 13 | 2 | ad2antrr 726 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑥 ∈ 𝑇 ∧ 𝑢 ∈ 𝑇)) ∧ (𝑦 ∈ 𝑈 ∧ 𝑣 ∈ 𝑈)) → 𝑈 ∈ (SubGrp‘𝐺)) |
| 14 | | pj1eu.4 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑇 ∩ 𝑈) = { 0 }) |
| 15 | 14 | ad2antrr 726 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑥 ∈ 𝑇 ∧ 𝑢 ∈ 𝑇)) ∧ (𝑦 ∈ 𝑈 ∧ 𝑣 ∈ 𝑈)) → (𝑇 ∩ 𝑈) = { 0 }) |
| 16 | | pj1eu.5 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑇 ⊆ (𝑍‘𝑈)) |
| 17 | 16 | ad2antrr 726 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑥 ∈ 𝑇 ∧ 𝑢 ∈ 𝑇)) ∧ (𝑦 ∈ 𝑈 ∧ 𝑣 ∈ 𝑈)) → 𝑇 ⊆ (𝑍‘𝑈)) |
| 18 | | simplrl 777 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑥 ∈ 𝑇 ∧ 𝑢 ∈ 𝑇)) ∧ (𝑦 ∈ 𝑈 ∧ 𝑣 ∈ 𝑈)) → 𝑥 ∈ 𝑇) |
| 19 | | simplrr 778 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑥 ∈ 𝑇 ∧ 𝑢 ∈ 𝑇)) ∧ (𝑦 ∈ 𝑈 ∧ 𝑣 ∈ 𝑈)) → 𝑢 ∈ 𝑇) |
| 20 | | simprl 771 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑥 ∈ 𝑇 ∧ 𝑢 ∈ 𝑇)) ∧ (𝑦 ∈ 𝑈 ∧ 𝑣 ∈ 𝑈)) → 𝑦 ∈ 𝑈) |
| 21 | | simprr 773 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑥 ∈ 𝑇 ∧ 𝑢 ∈ 𝑇)) ∧ (𝑦 ∈ 𝑈 ∧ 𝑣 ∈ 𝑈)) → 𝑣 ∈ 𝑈) |
| 22 | 3, 10, 11, 12, 13, 15, 17, 18, 19, 20, 21 | subgdisjb 19711 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑥 ∈ 𝑇 ∧ 𝑢 ∈ 𝑇)) ∧ (𝑦 ∈ 𝑈 ∧ 𝑣 ∈ 𝑈)) → ((𝑥 + 𝑦) = (𝑢 + 𝑣) ↔ (𝑥 = 𝑢 ∧ 𝑦 = 𝑣))) |
| 23 | | simpl 482 |
. . . . . . . 8
⊢ ((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → 𝑥 = 𝑢) |
| 24 | 22, 23 | biimtrdi 253 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑥 ∈ 𝑇 ∧ 𝑢 ∈ 𝑇)) ∧ (𝑦 ∈ 𝑈 ∧ 𝑣 ∈ 𝑈)) → ((𝑥 + 𝑦) = (𝑢 + 𝑣) → 𝑥 = 𝑢)) |
| 25 | 9, 24 | syl5 34 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑥 ∈ 𝑇 ∧ 𝑢 ∈ 𝑇)) ∧ (𝑦 ∈ 𝑈 ∧ 𝑣 ∈ 𝑈)) → ((𝑋 = (𝑥 + 𝑦) ∧ 𝑋 = (𝑢 + 𝑣)) → 𝑥 = 𝑢)) |
| 26 | 25 | rexlimdvva 3213 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑇 ∧ 𝑢 ∈ 𝑇)) → (∃𝑦 ∈ 𝑈 ∃𝑣 ∈ 𝑈 (𝑋 = (𝑥 + 𝑦) ∧ 𝑋 = (𝑢 + 𝑣)) → 𝑥 = 𝑢)) |
| 27 | 8, 26 | biimtrrid 243 |
. . . 4
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑇 ∧ 𝑢 ∈ 𝑇)) → ((∃𝑦 ∈ 𝑈 𝑋 = (𝑥 + 𝑦) ∧ ∃𝑣 ∈ 𝑈 𝑋 = (𝑢 + 𝑣)) → 𝑥 = 𝑢)) |
| 28 | 27 | ralrimivva 3202 |
. . 3
⊢ (𝜑 → ∀𝑥 ∈ 𝑇 ∀𝑢 ∈ 𝑇 ((∃𝑦 ∈ 𝑈 𝑋 = (𝑥 + 𝑦) ∧ ∃𝑣 ∈ 𝑈 𝑋 = (𝑢 + 𝑣)) → 𝑥 = 𝑢)) |
| 29 | 28 | adantr 480 |
. 2
⊢ ((𝜑 ∧ 𝑋 ∈ (𝑇 ⊕ 𝑈)) → ∀𝑥 ∈ 𝑇 ∀𝑢 ∈ 𝑇 ((∃𝑦 ∈ 𝑈 𝑋 = (𝑥 + 𝑦) ∧ ∃𝑣 ∈ 𝑈 𝑋 = (𝑢 + 𝑣)) → 𝑥 = 𝑢)) |
| 30 | | oveq1 7438 |
. . . . . 6
⊢ (𝑥 = 𝑢 → (𝑥 + 𝑦) = (𝑢 + 𝑦)) |
| 31 | 30 | eqeq2d 2748 |
. . . . 5
⊢ (𝑥 = 𝑢 → (𝑋 = (𝑥 + 𝑦) ↔ 𝑋 = (𝑢 + 𝑦))) |
| 32 | 31 | rexbidv 3179 |
. . . 4
⊢ (𝑥 = 𝑢 → (∃𝑦 ∈ 𝑈 𝑋 = (𝑥 + 𝑦) ↔ ∃𝑦 ∈ 𝑈 𝑋 = (𝑢 + 𝑦))) |
| 33 | | oveq2 7439 |
. . . . . 6
⊢ (𝑦 = 𝑣 → (𝑢 + 𝑦) = (𝑢 + 𝑣)) |
| 34 | 33 | eqeq2d 2748 |
. . . . 5
⊢ (𝑦 = 𝑣 → (𝑋 = (𝑢 + 𝑦) ↔ 𝑋 = (𝑢 + 𝑣))) |
| 35 | 34 | cbvrexvw 3238 |
. . . 4
⊢
(∃𝑦 ∈
𝑈 𝑋 = (𝑢 + 𝑦) ↔ ∃𝑣 ∈ 𝑈 𝑋 = (𝑢 + 𝑣)) |
| 36 | 32, 35 | bitrdi 287 |
. . 3
⊢ (𝑥 = 𝑢 → (∃𝑦 ∈ 𝑈 𝑋 = (𝑥 + 𝑦) ↔ ∃𝑣 ∈ 𝑈 𝑋 = (𝑢 + 𝑣))) |
| 37 | 36 | reu4 3737 |
. 2
⊢
(∃!𝑥 ∈
𝑇 ∃𝑦 ∈ 𝑈 𝑋 = (𝑥 + 𝑦) ↔ (∃𝑥 ∈ 𝑇 ∃𝑦 ∈ 𝑈 𝑋 = (𝑥 + 𝑦) ∧ ∀𝑥 ∈ 𝑇 ∀𝑢 ∈ 𝑇 ((∃𝑦 ∈ 𝑈 𝑋 = (𝑥 + 𝑦) ∧ ∃𝑣 ∈ 𝑈 𝑋 = (𝑢 + 𝑣)) → 𝑥 = 𝑢))) |
| 38 | 7, 29, 37 | sylanbrc 583 |
1
⊢ ((𝜑 ∧ 𝑋 ∈ (𝑇 ⊕ 𝑈)) → ∃!𝑥 ∈ 𝑇 ∃𝑦 ∈ 𝑈 𝑋 = (𝑥 + 𝑦)) |