Proof of Theorem eqgcpbl
| Step | Hyp | Ref
| Expression |
| 1 | | nsgsubg 19176 |
. . . . . 6
⊢ (𝑌 ∈ (NrmSGrp‘𝐺) → 𝑌 ∈ (SubGrp‘𝐺)) |
| 2 | 1 | adantr 480 |
. . . . 5
⊢ ((𝑌 ∈ (NrmSGrp‘𝐺) ∧ (𝐴 ∼ 𝐶 ∧ 𝐵 ∼ 𝐷)) → 𝑌 ∈ (SubGrp‘𝐺)) |
| 3 | | subgrcl 19149 |
. . . . 5
⊢ (𝑌 ∈ (SubGrp‘𝐺) → 𝐺 ∈ Grp) |
| 4 | 2, 3 | syl 17 |
. . . 4
⊢ ((𝑌 ∈ (NrmSGrp‘𝐺) ∧ (𝐴 ∼ 𝐶 ∧ 𝐵 ∼ 𝐷)) → 𝐺 ∈ Grp) |
| 5 | | simprl 771 |
. . . . . 6
⊢ ((𝑌 ∈ (NrmSGrp‘𝐺) ∧ (𝐴 ∼ 𝐶 ∧ 𝐵 ∼ 𝐷)) → 𝐴 ∼ 𝐶) |
| 6 | | eqger.x |
. . . . . . . . 9
⊢ 𝑋 = (Base‘𝐺) |
| 7 | 6 | subgss 19145 |
. . . . . . . 8
⊢ (𝑌 ∈ (SubGrp‘𝐺) → 𝑌 ⊆ 𝑋) |
| 8 | 2, 7 | syl 17 |
. . . . . . 7
⊢ ((𝑌 ∈ (NrmSGrp‘𝐺) ∧ (𝐴 ∼ 𝐶 ∧ 𝐵 ∼ 𝐷)) → 𝑌 ⊆ 𝑋) |
| 9 | | eqid 2737 |
. . . . . . . 8
⊢
(invg‘𝐺) = (invg‘𝐺) |
| 10 | | eqgcpbl.p |
. . . . . . . 8
⊢ + =
(+g‘𝐺) |
| 11 | | eqger.r |
. . . . . . . 8
⊢ ∼ =
(𝐺 ~QG
𝑌) |
| 12 | 6, 9, 10, 11 | eqgval 19195 |
. . . . . . 7
⊢ ((𝐺 ∈ Grp ∧ 𝑌 ⊆ 𝑋) → (𝐴 ∼ 𝐶 ↔ (𝐴 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ∧ (((invg‘𝐺)‘𝐴) + 𝐶) ∈ 𝑌))) |
| 13 | 4, 8, 12 | syl2anc 584 |
. . . . . 6
⊢ ((𝑌 ∈ (NrmSGrp‘𝐺) ∧ (𝐴 ∼ 𝐶 ∧ 𝐵 ∼ 𝐷)) → (𝐴 ∼ 𝐶 ↔ (𝐴 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ∧ (((invg‘𝐺)‘𝐴) + 𝐶) ∈ 𝑌))) |
| 14 | 5, 13 | mpbid 232 |
. . . . 5
⊢ ((𝑌 ∈ (NrmSGrp‘𝐺) ∧ (𝐴 ∼ 𝐶 ∧ 𝐵 ∼ 𝐷)) → (𝐴 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ∧ (((invg‘𝐺)‘𝐴) + 𝐶) ∈ 𝑌)) |
| 15 | 14 | simp1d 1143 |
. . . 4
⊢ ((𝑌 ∈ (NrmSGrp‘𝐺) ∧ (𝐴 ∼ 𝐶 ∧ 𝐵 ∼ 𝐷)) → 𝐴 ∈ 𝑋) |
| 16 | | simprr 773 |
. . . . . 6
⊢ ((𝑌 ∈ (NrmSGrp‘𝐺) ∧ (𝐴 ∼ 𝐶 ∧ 𝐵 ∼ 𝐷)) → 𝐵 ∼ 𝐷) |
| 17 | 6, 9, 10, 11 | eqgval 19195 |
. . . . . . 7
⊢ ((𝐺 ∈ Grp ∧ 𝑌 ⊆ 𝑋) → (𝐵 ∼ 𝐷 ↔ (𝐵 ∈ 𝑋 ∧ 𝐷 ∈ 𝑋 ∧ (((invg‘𝐺)‘𝐵) + 𝐷) ∈ 𝑌))) |
| 18 | 4, 8, 17 | syl2anc 584 |
. . . . . 6
⊢ ((𝑌 ∈ (NrmSGrp‘𝐺) ∧ (𝐴 ∼ 𝐶 ∧ 𝐵 ∼ 𝐷)) → (𝐵 ∼ 𝐷 ↔ (𝐵 ∈ 𝑋 ∧ 𝐷 ∈ 𝑋 ∧ (((invg‘𝐺)‘𝐵) + 𝐷) ∈ 𝑌))) |
| 19 | 16, 18 | mpbid 232 |
. . . . 5
⊢ ((𝑌 ∈ (NrmSGrp‘𝐺) ∧ (𝐴 ∼ 𝐶 ∧ 𝐵 ∼ 𝐷)) → (𝐵 ∈ 𝑋 ∧ 𝐷 ∈ 𝑋 ∧ (((invg‘𝐺)‘𝐵) + 𝐷) ∈ 𝑌)) |
| 20 | 19 | simp1d 1143 |
. . . 4
⊢ ((𝑌 ∈ (NrmSGrp‘𝐺) ∧ (𝐴 ∼ 𝐶 ∧ 𝐵 ∼ 𝐷)) → 𝐵 ∈ 𝑋) |
| 21 | 6, 10 | grpcl 18959 |
. . . 4
⊢ ((𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐴 + 𝐵) ∈ 𝑋) |
| 22 | 4, 15, 20, 21 | syl3anc 1373 |
. . 3
⊢ ((𝑌 ∈ (NrmSGrp‘𝐺) ∧ (𝐴 ∼ 𝐶 ∧ 𝐵 ∼ 𝐷)) → (𝐴 + 𝐵) ∈ 𝑋) |
| 23 | 14 | simp2d 1144 |
. . . 4
⊢ ((𝑌 ∈ (NrmSGrp‘𝐺) ∧ (𝐴 ∼ 𝐶 ∧ 𝐵 ∼ 𝐷)) → 𝐶 ∈ 𝑋) |
| 24 | 19 | simp2d 1144 |
. . . 4
⊢ ((𝑌 ∈ (NrmSGrp‘𝐺) ∧ (𝐴 ∼ 𝐶 ∧ 𝐵 ∼ 𝐷)) → 𝐷 ∈ 𝑋) |
| 25 | 6, 10 | grpcl 18959 |
. . . 4
⊢ ((𝐺 ∈ Grp ∧ 𝐶 ∈ 𝑋 ∧ 𝐷 ∈ 𝑋) → (𝐶 + 𝐷) ∈ 𝑋) |
| 26 | 4, 23, 24, 25 | syl3anc 1373 |
. . 3
⊢ ((𝑌 ∈ (NrmSGrp‘𝐺) ∧ (𝐴 ∼ 𝐶 ∧ 𝐵 ∼ 𝐷)) → (𝐶 + 𝐷) ∈ 𝑋) |
| 27 | 6, 10, 9 | grpinvadd 19036 |
. . . . . . 7
⊢ ((𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → ((invg‘𝐺)‘(𝐴 + 𝐵)) = (((invg‘𝐺)‘𝐵) +
((invg‘𝐺)‘𝐴))) |
| 28 | 4, 15, 20, 27 | syl3anc 1373 |
. . . . . 6
⊢ ((𝑌 ∈ (NrmSGrp‘𝐺) ∧ (𝐴 ∼ 𝐶 ∧ 𝐵 ∼ 𝐷)) → ((invg‘𝐺)‘(𝐴 + 𝐵)) = (((invg‘𝐺)‘𝐵) +
((invg‘𝐺)‘𝐴))) |
| 29 | 28 | oveq1d 7446 |
. . . . 5
⊢ ((𝑌 ∈ (NrmSGrp‘𝐺) ∧ (𝐴 ∼ 𝐶 ∧ 𝐵 ∼ 𝐷)) → (((invg‘𝐺)‘(𝐴 + 𝐵)) + (𝐶 + 𝐷)) = ((((invg‘𝐺)‘𝐵) +
((invg‘𝐺)‘𝐴)) + (𝐶 + 𝐷))) |
| 30 | 6, 9 | grpinvcl 19005 |
. . . . . . 7
⊢ ((𝐺 ∈ Grp ∧ 𝐵 ∈ 𝑋) → ((invg‘𝐺)‘𝐵) ∈ 𝑋) |
| 31 | 4, 20, 30 | syl2anc 584 |
. . . . . 6
⊢ ((𝑌 ∈ (NrmSGrp‘𝐺) ∧ (𝐴 ∼ 𝐶 ∧ 𝐵 ∼ 𝐷)) → ((invg‘𝐺)‘𝐵) ∈ 𝑋) |
| 32 | 6, 9 | grpinvcl 19005 |
. . . . . . 7
⊢ ((𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋) → ((invg‘𝐺)‘𝐴) ∈ 𝑋) |
| 33 | 4, 15, 32 | syl2anc 584 |
. . . . . 6
⊢ ((𝑌 ∈ (NrmSGrp‘𝐺) ∧ (𝐴 ∼ 𝐶 ∧ 𝐵 ∼ 𝐷)) → ((invg‘𝐺)‘𝐴) ∈ 𝑋) |
| 34 | 6, 10 | grpass 18960 |
. . . . . 6
⊢ ((𝐺 ∈ Grp ∧
(((invg‘𝐺)‘𝐵) ∈ 𝑋 ∧ ((invg‘𝐺)‘𝐴) ∈ 𝑋 ∧ (𝐶 + 𝐷) ∈ 𝑋)) → ((((invg‘𝐺)‘𝐵) +
((invg‘𝐺)‘𝐴)) + (𝐶 + 𝐷)) = (((invg‘𝐺)‘𝐵) +
(((invg‘𝐺)‘𝐴) + (𝐶 + 𝐷)))) |
| 35 | 4, 31, 33, 26, 34 | syl13anc 1374 |
. . . . 5
⊢ ((𝑌 ∈ (NrmSGrp‘𝐺) ∧ (𝐴 ∼ 𝐶 ∧ 𝐵 ∼ 𝐷)) → ((((invg‘𝐺)‘𝐵) +
((invg‘𝐺)‘𝐴)) + (𝐶 + 𝐷)) = (((invg‘𝐺)‘𝐵) +
(((invg‘𝐺)‘𝐴) + (𝐶 + 𝐷)))) |
| 36 | 29, 35 | eqtrd 2777 |
. . . 4
⊢ ((𝑌 ∈ (NrmSGrp‘𝐺) ∧ (𝐴 ∼ 𝐶 ∧ 𝐵 ∼ 𝐷)) → (((invg‘𝐺)‘(𝐴 + 𝐵)) + (𝐶 + 𝐷)) = (((invg‘𝐺)‘𝐵) +
(((invg‘𝐺)‘𝐴) + (𝐶 + 𝐷)))) |
| 37 | 6, 10 | grpass 18960 |
. . . . . . . . 9
⊢ ((𝐺 ∈ Grp ∧
(((invg‘𝐺)‘𝐴) ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ∧ 𝐷 ∈ 𝑋)) → ((((invg‘𝐺)‘𝐴) + 𝐶) + 𝐷) = (((invg‘𝐺)‘𝐴) + (𝐶 + 𝐷))) |
| 38 | 4, 33, 23, 24, 37 | syl13anc 1374 |
. . . . . . . 8
⊢ ((𝑌 ∈ (NrmSGrp‘𝐺) ∧ (𝐴 ∼ 𝐶 ∧ 𝐵 ∼ 𝐷)) → ((((invg‘𝐺)‘𝐴) + 𝐶) + 𝐷) = (((invg‘𝐺)‘𝐴) + (𝐶 + 𝐷))) |
| 39 | 38 | oveq1d 7446 |
. . . . . . 7
⊢ ((𝑌 ∈ (NrmSGrp‘𝐺) ∧ (𝐴 ∼ 𝐶 ∧ 𝐵 ∼ 𝐷)) → (((((invg‘𝐺)‘𝐴) + 𝐶) + 𝐷) +
((invg‘𝐺)‘𝐵)) = ((((invg‘𝐺)‘𝐴) + (𝐶 + 𝐷)) +
((invg‘𝐺)‘𝐵))) |
| 40 | 6, 10 | grpcl 18959 |
. . . . . . . . 9
⊢ ((𝐺 ∈ Grp ∧
((invg‘𝐺)‘𝐴) ∈ 𝑋 ∧ 𝐶 ∈ 𝑋) → (((invg‘𝐺)‘𝐴) + 𝐶) ∈ 𝑋) |
| 41 | 4, 33, 23, 40 | syl3anc 1373 |
. . . . . . . 8
⊢ ((𝑌 ∈ (NrmSGrp‘𝐺) ∧ (𝐴 ∼ 𝐶 ∧ 𝐵 ∼ 𝐷)) → (((invg‘𝐺)‘𝐴) + 𝐶) ∈ 𝑋) |
| 42 | 6, 10 | grpass 18960 |
. . . . . . . 8
⊢ ((𝐺 ∈ Grp ∧
((((invg‘𝐺)‘𝐴) + 𝐶) ∈ 𝑋 ∧ 𝐷 ∈ 𝑋 ∧ ((invg‘𝐺)‘𝐵) ∈ 𝑋)) → (((((invg‘𝐺)‘𝐴) + 𝐶) + 𝐷) +
((invg‘𝐺)‘𝐵)) = ((((invg‘𝐺)‘𝐴) + 𝐶) + (𝐷 +
((invg‘𝐺)‘𝐵)))) |
| 43 | 4, 41, 24, 31, 42 | syl13anc 1374 |
. . . . . . 7
⊢ ((𝑌 ∈ (NrmSGrp‘𝐺) ∧ (𝐴 ∼ 𝐶 ∧ 𝐵 ∼ 𝐷)) → (((((invg‘𝐺)‘𝐴) + 𝐶) + 𝐷) +
((invg‘𝐺)‘𝐵)) = ((((invg‘𝐺)‘𝐴) + 𝐶) + (𝐷 +
((invg‘𝐺)‘𝐵)))) |
| 44 | 39, 43 | eqtr3d 2779 |
. . . . . 6
⊢ ((𝑌 ∈ (NrmSGrp‘𝐺) ∧ (𝐴 ∼ 𝐶 ∧ 𝐵 ∼ 𝐷)) → ((((invg‘𝐺)‘𝐴) + (𝐶 + 𝐷)) +
((invg‘𝐺)‘𝐵)) = ((((invg‘𝐺)‘𝐴) + 𝐶) + (𝐷 +
((invg‘𝐺)‘𝐵)))) |
| 45 | 14 | simp3d 1145 |
. . . . . . 7
⊢ ((𝑌 ∈ (NrmSGrp‘𝐺) ∧ (𝐴 ∼ 𝐶 ∧ 𝐵 ∼ 𝐷)) → (((invg‘𝐺)‘𝐴) + 𝐶) ∈ 𝑌) |
| 46 | 19 | simp3d 1145 |
. . . . . . . 8
⊢ ((𝑌 ∈ (NrmSGrp‘𝐺) ∧ (𝐴 ∼ 𝐶 ∧ 𝐵 ∼ 𝐷)) → (((invg‘𝐺)‘𝐵) + 𝐷) ∈ 𝑌) |
| 47 | | simpl 482 |
. . . . . . . . 9
⊢ ((𝑌 ∈ (NrmSGrp‘𝐺) ∧ (𝐴 ∼ 𝐶 ∧ 𝐵 ∼ 𝐷)) → 𝑌 ∈ (NrmSGrp‘𝐺)) |
| 48 | 6, 10 | nsgbi 19175 |
. . . . . . . . 9
⊢ ((𝑌 ∈ (NrmSGrp‘𝐺) ∧
((invg‘𝐺)‘𝐵) ∈ 𝑋 ∧ 𝐷 ∈ 𝑋) → ((((invg‘𝐺)‘𝐵) + 𝐷) ∈ 𝑌 ↔ (𝐷 +
((invg‘𝐺)‘𝐵)) ∈ 𝑌)) |
| 49 | 47, 31, 24, 48 | syl3anc 1373 |
. . . . . . . 8
⊢ ((𝑌 ∈ (NrmSGrp‘𝐺) ∧ (𝐴 ∼ 𝐶 ∧ 𝐵 ∼ 𝐷)) → ((((invg‘𝐺)‘𝐵) + 𝐷) ∈ 𝑌 ↔ (𝐷 +
((invg‘𝐺)‘𝐵)) ∈ 𝑌)) |
| 50 | 46, 49 | mpbid 232 |
. . . . . . 7
⊢ ((𝑌 ∈ (NrmSGrp‘𝐺) ∧ (𝐴 ∼ 𝐶 ∧ 𝐵 ∼ 𝐷)) → (𝐷 +
((invg‘𝐺)‘𝐵)) ∈ 𝑌) |
| 51 | 10 | subgcl 19154 |
. . . . . . 7
⊢ ((𝑌 ∈ (SubGrp‘𝐺) ∧
(((invg‘𝐺)‘𝐴) + 𝐶) ∈ 𝑌 ∧ (𝐷 +
((invg‘𝐺)‘𝐵)) ∈ 𝑌) → ((((invg‘𝐺)‘𝐴) + 𝐶) + (𝐷 +
((invg‘𝐺)‘𝐵))) ∈ 𝑌) |
| 52 | 2, 45, 50, 51 | syl3anc 1373 |
. . . . . 6
⊢ ((𝑌 ∈ (NrmSGrp‘𝐺) ∧ (𝐴 ∼ 𝐶 ∧ 𝐵 ∼ 𝐷)) → ((((invg‘𝐺)‘𝐴) + 𝐶) + (𝐷 +
((invg‘𝐺)‘𝐵))) ∈ 𝑌) |
| 53 | 44, 52 | eqeltrd 2841 |
. . . . 5
⊢ ((𝑌 ∈ (NrmSGrp‘𝐺) ∧ (𝐴 ∼ 𝐶 ∧ 𝐵 ∼ 𝐷)) → ((((invg‘𝐺)‘𝐴) + (𝐶 + 𝐷)) +
((invg‘𝐺)‘𝐵)) ∈ 𝑌) |
| 54 | 6, 10 | grpcl 18959 |
. . . . . . 7
⊢ ((𝐺 ∈ Grp ∧
((invg‘𝐺)‘𝐴) ∈ 𝑋 ∧ (𝐶 + 𝐷) ∈ 𝑋) → (((invg‘𝐺)‘𝐴) + (𝐶 + 𝐷)) ∈ 𝑋) |
| 55 | 4, 33, 26, 54 | syl3anc 1373 |
. . . . . 6
⊢ ((𝑌 ∈ (NrmSGrp‘𝐺) ∧ (𝐴 ∼ 𝐶 ∧ 𝐵 ∼ 𝐷)) → (((invg‘𝐺)‘𝐴) + (𝐶 + 𝐷)) ∈ 𝑋) |
| 56 | 6, 10 | nsgbi 19175 |
. . . . . 6
⊢ ((𝑌 ∈ (NrmSGrp‘𝐺) ∧
(((invg‘𝐺)‘𝐴) + (𝐶 + 𝐷)) ∈ 𝑋 ∧ ((invg‘𝐺)‘𝐵) ∈ 𝑋) → (((((invg‘𝐺)‘𝐴) + (𝐶 + 𝐷)) +
((invg‘𝐺)‘𝐵)) ∈ 𝑌 ↔ (((invg‘𝐺)‘𝐵) +
(((invg‘𝐺)‘𝐴) + (𝐶 + 𝐷))) ∈ 𝑌)) |
| 57 | 47, 55, 31, 56 | syl3anc 1373 |
. . . . 5
⊢ ((𝑌 ∈ (NrmSGrp‘𝐺) ∧ (𝐴 ∼ 𝐶 ∧ 𝐵 ∼ 𝐷)) → (((((invg‘𝐺)‘𝐴) + (𝐶 + 𝐷)) +
((invg‘𝐺)‘𝐵)) ∈ 𝑌 ↔ (((invg‘𝐺)‘𝐵) +
(((invg‘𝐺)‘𝐴) + (𝐶 + 𝐷))) ∈ 𝑌)) |
| 58 | 53, 57 | mpbid 232 |
. . . 4
⊢ ((𝑌 ∈ (NrmSGrp‘𝐺) ∧ (𝐴 ∼ 𝐶 ∧ 𝐵 ∼ 𝐷)) → (((invg‘𝐺)‘𝐵) +
(((invg‘𝐺)‘𝐴) + (𝐶 + 𝐷))) ∈ 𝑌) |
| 59 | 36, 58 | eqeltrd 2841 |
. . 3
⊢ ((𝑌 ∈ (NrmSGrp‘𝐺) ∧ (𝐴 ∼ 𝐶 ∧ 𝐵 ∼ 𝐷)) → (((invg‘𝐺)‘(𝐴 + 𝐵)) + (𝐶 + 𝐷)) ∈ 𝑌) |
| 60 | 6, 9, 10, 11 | eqgval 19195 |
. . . 4
⊢ ((𝐺 ∈ Grp ∧ 𝑌 ⊆ 𝑋) → ((𝐴 + 𝐵) ∼ (𝐶 + 𝐷) ↔ ((𝐴 + 𝐵) ∈ 𝑋 ∧ (𝐶 + 𝐷) ∈ 𝑋 ∧ (((invg‘𝐺)‘(𝐴 + 𝐵)) + (𝐶 + 𝐷)) ∈ 𝑌))) |
| 61 | 4, 8, 60 | syl2anc 584 |
. . 3
⊢ ((𝑌 ∈ (NrmSGrp‘𝐺) ∧ (𝐴 ∼ 𝐶 ∧ 𝐵 ∼ 𝐷)) → ((𝐴 + 𝐵) ∼ (𝐶 + 𝐷) ↔ ((𝐴 + 𝐵) ∈ 𝑋 ∧ (𝐶 + 𝐷) ∈ 𝑋 ∧ (((invg‘𝐺)‘(𝐴 + 𝐵)) + (𝐶 + 𝐷)) ∈ 𝑌))) |
| 62 | 22, 26, 59, 61 | mpbir3and 1343 |
. 2
⊢ ((𝑌 ∈ (NrmSGrp‘𝐺) ∧ (𝐴 ∼ 𝐶 ∧ 𝐵 ∼ 𝐷)) → (𝐴 + 𝐵) ∼ (𝐶 + 𝐷)) |
| 63 | 62 | ex 412 |
1
⊢ (𝑌 ∈ (NrmSGrp‘𝐺) → ((𝐴 ∼ 𝐶 ∧ 𝐵 ∼ 𝐷) → (𝐴 + 𝐵) ∼ (𝐶 + 𝐷))) |