Proof of Theorem galcan
Step | Hyp | Ref
| Expression |
1 | | oveq2 7263 |
. . 3
⊢ ((𝐴 ⊕ 𝐵) = (𝐴 ⊕ 𝐶) → (((invg‘𝐺)‘𝐴) ⊕ (𝐴 ⊕ 𝐵)) = (((invg‘𝐺)‘𝐴) ⊕ (𝐴 ⊕ 𝐶))) |
2 | | simpl 482 |
. . . . . . . 8
⊢ (( ⊕ ∈
(𝐺 GrpAct 𝑌) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑌)) → ⊕ ∈ (𝐺 GrpAct 𝑌)) |
3 | | gagrp 18813 |
. . . . . . . 8
⊢ ( ⊕ ∈
(𝐺 GrpAct 𝑌) → 𝐺 ∈ Grp) |
4 | 2, 3 | syl 17 |
. . . . . . 7
⊢ (( ⊕ ∈
(𝐺 GrpAct 𝑌) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑌)) → 𝐺 ∈ Grp) |
5 | | simpr1 1192 |
. . . . . . 7
⊢ (( ⊕ ∈
(𝐺 GrpAct 𝑌) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑌)) → 𝐴 ∈ 𝑋) |
6 | | galcan.1 |
. . . . . . . 8
⊢ 𝑋 = (Base‘𝐺) |
7 | | eqid 2738 |
. . . . . . . 8
⊢
(+g‘𝐺) = (+g‘𝐺) |
8 | | eqid 2738 |
. . . . . . . 8
⊢
(0g‘𝐺) = (0g‘𝐺) |
9 | | eqid 2738 |
. . . . . . . 8
⊢
(invg‘𝐺) = (invg‘𝐺) |
10 | 6, 7, 8, 9 | grplinv 18543 |
. . . . . . 7
⊢ ((𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋) → (((invg‘𝐺)‘𝐴)(+g‘𝐺)𝐴) = (0g‘𝐺)) |
11 | 4, 5, 10 | syl2anc 583 |
. . . . . 6
⊢ (( ⊕ ∈
(𝐺 GrpAct 𝑌) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑌)) → (((invg‘𝐺)‘𝐴)(+g‘𝐺)𝐴) = (0g‘𝐺)) |
12 | 11 | oveq1d 7270 |
. . . . 5
⊢ (( ⊕ ∈
(𝐺 GrpAct 𝑌) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑌)) → ((((invg‘𝐺)‘𝐴)(+g‘𝐺)𝐴) ⊕ 𝐵) = ((0g‘𝐺) ⊕ 𝐵)) |
13 | 6, 9 | grpinvcl 18542 |
. . . . . . 7
⊢ ((𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋) → ((invg‘𝐺)‘𝐴) ∈ 𝑋) |
14 | 4, 5, 13 | syl2anc 583 |
. . . . . 6
⊢ (( ⊕ ∈
(𝐺 GrpAct 𝑌) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑌)) → ((invg‘𝐺)‘𝐴) ∈ 𝑋) |
15 | | simpr2 1193 |
. . . . . 6
⊢ (( ⊕ ∈
(𝐺 GrpAct 𝑌) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑌)) → 𝐵 ∈ 𝑌) |
16 | 6, 7 | gaass 18818 |
. . . . . 6
⊢ (( ⊕ ∈
(𝐺 GrpAct 𝑌) ∧ (((invg‘𝐺)‘𝐴) ∈ 𝑋 ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌)) → ((((invg‘𝐺)‘𝐴)(+g‘𝐺)𝐴) ⊕ 𝐵) = (((invg‘𝐺)‘𝐴) ⊕ (𝐴 ⊕ 𝐵))) |
17 | 2, 14, 5, 15, 16 | syl13anc 1370 |
. . . . 5
⊢ (( ⊕ ∈
(𝐺 GrpAct 𝑌) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑌)) → ((((invg‘𝐺)‘𝐴)(+g‘𝐺)𝐴) ⊕ 𝐵) = (((invg‘𝐺)‘𝐴) ⊕ (𝐴 ⊕ 𝐵))) |
18 | 8 | gagrpid 18815 |
. . . . . 6
⊢ (( ⊕ ∈
(𝐺 GrpAct 𝑌) ∧ 𝐵 ∈ 𝑌) → ((0g‘𝐺) ⊕ 𝐵) = 𝐵) |
19 | 2, 15, 18 | syl2anc 583 |
. . . . 5
⊢ (( ⊕ ∈
(𝐺 GrpAct 𝑌) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑌)) → ((0g‘𝐺) ⊕ 𝐵) = 𝐵) |
20 | 12, 17, 19 | 3eqtr3d 2786 |
. . . 4
⊢ (( ⊕ ∈
(𝐺 GrpAct 𝑌) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑌)) → (((invg‘𝐺)‘𝐴) ⊕ (𝐴 ⊕ 𝐵)) = 𝐵) |
21 | 11 | oveq1d 7270 |
. . . . 5
⊢ (( ⊕ ∈
(𝐺 GrpAct 𝑌) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑌)) → ((((invg‘𝐺)‘𝐴)(+g‘𝐺)𝐴) ⊕ 𝐶) = ((0g‘𝐺) ⊕ 𝐶)) |
22 | | simpr3 1194 |
. . . . . 6
⊢ (( ⊕ ∈
(𝐺 GrpAct 𝑌) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑌)) → 𝐶 ∈ 𝑌) |
23 | 6, 7 | gaass 18818 |
. . . . . 6
⊢ (( ⊕ ∈
(𝐺 GrpAct 𝑌) ∧ (((invg‘𝐺)‘𝐴) ∈ 𝑋 ∧ 𝐴 ∈ 𝑋 ∧ 𝐶 ∈ 𝑌)) → ((((invg‘𝐺)‘𝐴)(+g‘𝐺)𝐴) ⊕ 𝐶) = (((invg‘𝐺)‘𝐴) ⊕ (𝐴 ⊕ 𝐶))) |
24 | 2, 14, 5, 22, 23 | syl13anc 1370 |
. . . . 5
⊢ (( ⊕ ∈
(𝐺 GrpAct 𝑌) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑌)) → ((((invg‘𝐺)‘𝐴)(+g‘𝐺)𝐴) ⊕ 𝐶) = (((invg‘𝐺)‘𝐴) ⊕ (𝐴 ⊕ 𝐶))) |
25 | 8 | gagrpid 18815 |
. . . . . 6
⊢ (( ⊕ ∈
(𝐺 GrpAct 𝑌) ∧ 𝐶 ∈ 𝑌) → ((0g‘𝐺) ⊕ 𝐶) = 𝐶) |
26 | 2, 22, 25 | syl2anc 583 |
. . . . 5
⊢ (( ⊕ ∈
(𝐺 GrpAct 𝑌) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑌)) → ((0g‘𝐺) ⊕ 𝐶) = 𝐶) |
27 | 21, 24, 26 | 3eqtr3d 2786 |
. . . 4
⊢ (( ⊕ ∈
(𝐺 GrpAct 𝑌) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑌)) → (((invg‘𝐺)‘𝐴) ⊕ (𝐴 ⊕ 𝐶)) = 𝐶) |
28 | 20, 27 | eqeq12d 2754 |
. . 3
⊢ (( ⊕ ∈
(𝐺 GrpAct 𝑌) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑌)) → ((((invg‘𝐺)‘𝐴) ⊕ (𝐴 ⊕ 𝐵)) = (((invg‘𝐺)‘𝐴) ⊕ (𝐴 ⊕ 𝐶)) ↔ 𝐵 = 𝐶)) |
29 | 1, 28 | syl5ib 243 |
. 2
⊢ (( ⊕ ∈
(𝐺 GrpAct 𝑌) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑌)) → ((𝐴 ⊕ 𝐵) = (𝐴 ⊕ 𝐶) → 𝐵 = 𝐶)) |
30 | | oveq2 7263 |
. 2
⊢ (𝐵 = 𝐶 → (𝐴 ⊕ 𝐵) = (𝐴 ⊕ 𝐶)) |
31 | 29, 30 | impbid1 224 |
1
⊢ (( ⊕ ∈
(𝐺 GrpAct 𝑌) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑌)) → ((𝐴 ⊕ 𝐵) = (𝐴 ⊕ 𝐶) ↔ 𝐵 = 𝐶)) |