Proof of Theorem gacan
| Step | Hyp | Ref
| Expression |
| 1 | | gagrp 19310 |
. . . . . . . 8
⊢ ( ⊕ ∈
(𝐺 GrpAct 𝑌) → 𝐺 ∈ Grp) |
| 2 | 1 | adantr 480 |
. . . . . . 7
⊢ (( ⊕ ∈
(𝐺 GrpAct 𝑌) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑌)) → 𝐺 ∈ Grp) |
| 3 | | simpr1 1195 |
. . . . . . 7
⊢ (( ⊕ ∈
(𝐺 GrpAct 𝑌) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑌)) → 𝐴 ∈ 𝑋) |
| 4 | | galcan.1 |
. . . . . . . 8
⊢ 𝑋 = (Base‘𝐺) |
| 5 | | eqid 2737 |
. . . . . . . 8
⊢
(+g‘𝐺) = (+g‘𝐺) |
| 6 | | eqid 2737 |
. . . . . . . 8
⊢
(0g‘𝐺) = (0g‘𝐺) |
| 7 | | gacan.2 |
. . . . . . . 8
⊢ 𝑁 = (invg‘𝐺) |
| 8 | 4, 5, 6, 7 | grprinv 19008 |
. . . . . . 7
⊢ ((𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋) → (𝐴(+g‘𝐺)(𝑁‘𝐴)) = (0g‘𝐺)) |
| 9 | 2, 3, 8 | syl2anc 584 |
. . . . . 6
⊢ (( ⊕ ∈
(𝐺 GrpAct 𝑌) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑌)) → (𝐴(+g‘𝐺)(𝑁‘𝐴)) = (0g‘𝐺)) |
| 10 | 9 | oveq1d 7446 |
. . . . 5
⊢ (( ⊕ ∈
(𝐺 GrpAct 𝑌) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑌)) → ((𝐴(+g‘𝐺)(𝑁‘𝐴)) ⊕ 𝐶) = ((0g‘𝐺) ⊕ 𝐶)) |
| 11 | | simpl 482 |
. . . . . 6
⊢ (( ⊕ ∈
(𝐺 GrpAct 𝑌) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑌)) → ⊕ ∈ (𝐺 GrpAct 𝑌)) |
| 12 | 4, 7 | grpinvcl 19005 |
. . . . . . 7
⊢ ((𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋) → (𝑁‘𝐴) ∈ 𝑋) |
| 13 | 2, 3, 12 | syl2anc 584 |
. . . . . 6
⊢ (( ⊕ ∈
(𝐺 GrpAct 𝑌) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑌)) → (𝑁‘𝐴) ∈ 𝑋) |
| 14 | | simpr3 1197 |
. . . . . 6
⊢ (( ⊕ ∈
(𝐺 GrpAct 𝑌) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑌)) → 𝐶 ∈ 𝑌) |
| 15 | 4, 5 | gaass 19315 |
. . . . . 6
⊢ (( ⊕ ∈
(𝐺 GrpAct 𝑌) ∧ (𝐴 ∈ 𝑋 ∧ (𝑁‘𝐴) ∈ 𝑋 ∧ 𝐶 ∈ 𝑌)) → ((𝐴(+g‘𝐺)(𝑁‘𝐴)) ⊕ 𝐶) = (𝐴 ⊕ ((𝑁‘𝐴) ⊕ 𝐶))) |
| 16 | 11, 3, 13, 14, 15 | syl13anc 1374 |
. . . . 5
⊢ (( ⊕ ∈
(𝐺 GrpAct 𝑌) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑌)) → ((𝐴(+g‘𝐺)(𝑁‘𝐴)) ⊕ 𝐶) = (𝐴 ⊕ ((𝑁‘𝐴) ⊕ 𝐶))) |
| 17 | 6 | gagrpid 19312 |
. . . . . 6
⊢ (( ⊕ ∈
(𝐺 GrpAct 𝑌) ∧ 𝐶 ∈ 𝑌) → ((0g‘𝐺) ⊕ 𝐶) = 𝐶) |
| 18 | 11, 14, 17 | syl2anc 584 |
. . . . 5
⊢ (( ⊕ ∈
(𝐺 GrpAct 𝑌) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑌)) → ((0g‘𝐺) ⊕ 𝐶) = 𝐶) |
| 19 | 10, 16, 18 | 3eqtr3d 2785 |
. . . 4
⊢ (( ⊕ ∈
(𝐺 GrpAct 𝑌) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑌)) → (𝐴 ⊕ ((𝑁‘𝐴) ⊕ 𝐶)) = 𝐶) |
| 20 | 19 | eqeq2d 2748 |
. . 3
⊢ (( ⊕ ∈
(𝐺 GrpAct 𝑌) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑌)) → ((𝐴 ⊕ 𝐵) = (𝐴 ⊕ ((𝑁‘𝐴) ⊕ 𝐶)) ↔ (𝐴 ⊕ 𝐵) = 𝐶)) |
| 21 | | simpr2 1196 |
. . . 4
⊢ (( ⊕ ∈
(𝐺 GrpAct 𝑌) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑌)) → 𝐵 ∈ 𝑌) |
| 22 | 4 | gaf 19313 |
. . . . . 6
⊢ ( ⊕ ∈
(𝐺 GrpAct 𝑌) → ⊕ :(𝑋 × 𝑌)⟶𝑌) |
| 23 | 22 | adantr 480 |
. . . . 5
⊢ (( ⊕ ∈
(𝐺 GrpAct 𝑌) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑌)) → ⊕ :(𝑋 × 𝑌)⟶𝑌) |
| 24 | 23, 13, 14 | fovcdmd 7605 |
. . . 4
⊢ (( ⊕ ∈
(𝐺 GrpAct 𝑌) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑌)) → ((𝑁‘𝐴) ⊕ 𝐶) ∈ 𝑌) |
| 25 | 4 | galcan 19322 |
. . . 4
⊢ (( ⊕ ∈
(𝐺 GrpAct 𝑌) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ ((𝑁‘𝐴) ⊕ 𝐶) ∈ 𝑌)) → ((𝐴 ⊕ 𝐵) = (𝐴 ⊕ ((𝑁‘𝐴) ⊕ 𝐶)) ↔ 𝐵 = ((𝑁‘𝐴) ⊕ 𝐶))) |
| 26 | 11, 3, 21, 24, 25 | syl13anc 1374 |
. . 3
⊢ (( ⊕ ∈
(𝐺 GrpAct 𝑌) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑌)) → ((𝐴 ⊕ 𝐵) = (𝐴 ⊕ ((𝑁‘𝐴) ⊕ 𝐶)) ↔ 𝐵 = ((𝑁‘𝐴) ⊕ 𝐶))) |
| 27 | 20, 26 | bitr3d 281 |
. 2
⊢ (( ⊕ ∈
(𝐺 GrpAct 𝑌) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑌)) → ((𝐴 ⊕ 𝐵) = 𝐶 ↔ 𝐵 = ((𝑁‘𝐴) ⊕ 𝐶))) |
| 28 | | eqcom 2744 |
. 2
⊢ (𝐵 = ((𝑁‘𝐴) ⊕ 𝐶) ↔ ((𝑁‘𝐴) ⊕ 𝐶) = 𝐵) |
| 29 | 27, 28 | bitrdi 287 |
1
⊢ (( ⊕ ∈
(𝐺 GrpAct 𝑌) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑌)) → ((𝐴 ⊕ 𝐵) = 𝐶 ↔ ((𝑁‘𝐴) ⊕ 𝐶) = 𝐵)) |