This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem eqgcpbl

Description: The subgroup coset equivalence relation is compatible with addition when the subgroup is normal. (Contributed by Mario Carneiro, 14-Jun-2015)

Ref Expression
Hypotheses eqger.x ⊢ 𝑋 = ( Base ‘ 𝐺 )
eqger.r ⊢ ∼ = ( 𝐺 ~QG 𝑌 )
eqgcpbl.p ⊢ + = ( +g ‘ 𝐺 )
Assertion eqgcpbl ( 𝑌 ∈ ( NrmSGrp ‘ 𝐺 ) → ( ( 𝐴 ∼ 𝐶 ∧ 𝐵 ∼ 𝐷 ) → ( 𝐴 + 𝐵 ) ∼ ( 𝐶 + 𝐷 ) ) )

Proof

Step Hyp Ref Expression
1 eqger.x ⊢ 𝑋 = ( Base ‘ 𝐺 )
2 eqger.r ⊢ ∼ = ( 𝐺 ~QG 𝑌 )
3 eqgcpbl.p ⊢ + = ( +g ‘ 𝐺 )
4 nsgsubg ⊢ ( 𝑌 ∈ ( NrmSGrp ‘ 𝐺 ) → 𝑌 ∈ ( SubGrp ‘ 𝐺 ) )
5 4 adantr ⊢ ( ( 𝑌 ∈ ( NrmSGrp ‘ 𝐺 ) ∧ ( 𝐴 ∼ 𝐶 ∧ 𝐵 ∼ 𝐷 ) ) → 𝑌 ∈ ( SubGrp ‘ 𝐺 ) )
6 subgrcl ⊢ ( 𝑌 ∈ ( SubGrp ‘ 𝐺 ) → 𝐺 ∈ Grp )
7 5 6 syl ⊢ ( ( 𝑌 ∈ ( NrmSGrp ‘ 𝐺 ) ∧ ( 𝐴 ∼ 𝐶 ∧ 𝐵 ∼ 𝐷 ) ) → 𝐺 ∈ Grp )
8 simprl ⊢ ( ( 𝑌 ∈ ( NrmSGrp ‘ 𝐺 ) ∧ ( 𝐴 ∼ 𝐶 ∧ 𝐵 ∼ 𝐷 ) ) → 𝐴 ∼ 𝐶 )
9 1 subgss ⊢ ( 𝑌 ∈ ( SubGrp ‘ 𝐺 ) → 𝑌 ⊆ 𝑋 )
10 5 9 syl ⊢ ( ( 𝑌 ∈ ( NrmSGrp ‘ 𝐺 ) ∧ ( 𝐴 ∼ 𝐶 ∧ 𝐵 ∼ 𝐷 ) ) → 𝑌 ⊆ 𝑋 )
11 eqid ⊢ ( invg ‘ 𝐺 ) = ( invg ‘ 𝐺 )
12 1 11 3 2 eqgval ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑌 ⊆ 𝑋 ) → ( 𝐴 ∼ 𝐶 ↔ ( 𝐴 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ∧ ( ( ( invg ‘ 𝐺 ) ‘ 𝐴 ) + 𝐶 ) ∈ 𝑌 ) ) )
13 7 10 12 syl2anc ⊢ ( ( 𝑌 ∈ ( NrmSGrp ‘ 𝐺 ) ∧ ( 𝐴 ∼ 𝐶 ∧ 𝐵 ∼ 𝐷 ) ) → ( 𝐴 ∼ 𝐶 ↔ ( 𝐴 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ∧ ( ( ( invg ‘ 𝐺 ) ‘ 𝐴 ) + 𝐶 ) ∈ 𝑌 ) ) )
14 8 13 mpbid ⊢ ( ( 𝑌 ∈ ( NrmSGrp ‘ 𝐺 ) ∧ ( 𝐴 ∼ 𝐶 ∧ 𝐵 ∼ 𝐷 ) ) → ( 𝐴 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ∧ ( ( ( invg ‘ 𝐺 ) ‘ 𝐴 ) + 𝐶 ) ∈ 𝑌 ) )
15 14 simp1d ⊢ ( ( 𝑌 ∈ ( NrmSGrp ‘ 𝐺 ) ∧ ( 𝐴 ∼ 𝐶 ∧ 𝐵 ∼ 𝐷 ) ) → 𝐴 ∈ 𝑋 )
16 simprr ⊢ ( ( 𝑌 ∈ ( NrmSGrp ‘ 𝐺 ) ∧ ( 𝐴 ∼ 𝐶 ∧ 𝐵 ∼ 𝐷 ) ) → 𝐵 ∼ 𝐷 )
17 1 11 3 2 eqgval ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑌 ⊆ 𝑋 ) → ( 𝐵 ∼ 𝐷 ↔ ( 𝐵 ∈ 𝑋 ∧ 𝐷 ∈ 𝑋 ∧ ( ( ( invg ‘ 𝐺 ) ‘ 𝐵 ) + 𝐷 ) ∈ 𝑌 ) ) )
18 7 10 17 syl2anc ⊢ ( ( 𝑌 ∈ ( NrmSGrp ‘ 𝐺 ) ∧ ( 𝐴 ∼ 𝐶 ∧ 𝐵 ∼ 𝐷 ) ) → ( 𝐵 ∼ 𝐷 ↔ ( 𝐵 ∈ 𝑋 ∧ 𝐷 ∈ 𝑋 ∧ ( ( ( invg ‘ 𝐺 ) ‘ 𝐵 ) + 𝐷 ) ∈ 𝑌 ) ) )
19 16 18 mpbid ⊢ ( ( 𝑌 ∈ ( NrmSGrp ‘ 𝐺 ) ∧ ( 𝐴 ∼ 𝐶 ∧ 𝐵 ∼ 𝐷 ) ) → ( 𝐵 ∈ 𝑋 ∧ 𝐷 ∈ 𝑋 ∧ ( ( ( invg ‘ 𝐺 ) ‘ 𝐵 ) + 𝐷 ) ∈ 𝑌 ) )
20 19 simp1d ⊢ ( ( 𝑌 ∈ ( NrmSGrp ‘ 𝐺 ) ∧ ( 𝐴 ∼ 𝐶 ∧ 𝐵 ∼ 𝐷 ) ) → 𝐵 ∈ 𝑋 )
21 1 3 grpcl ⊢ ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝐴 + 𝐵 ) ∈ 𝑋 )
22 7 15 20 21 syl3anc ⊢ ( ( 𝑌 ∈ ( NrmSGrp ‘ 𝐺 ) ∧ ( 𝐴 ∼ 𝐶 ∧ 𝐵 ∼ 𝐷 ) ) → ( 𝐴 + 𝐵 ) ∈ 𝑋 )
23 14 simp2d ⊢ ( ( 𝑌 ∈ ( NrmSGrp ‘ 𝐺 ) ∧ ( 𝐴 ∼ 𝐶 ∧ 𝐵 ∼ 𝐷 ) ) → 𝐶 ∈ 𝑋 )
24 19 simp2d ⊢ ( ( 𝑌 ∈ ( NrmSGrp ‘ 𝐺 ) ∧ ( 𝐴 ∼ 𝐶 ∧ 𝐵 ∼ 𝐷 ) ) → 𝐷 ∈ 𝑋 )
25 1 3 grpcl ⊢ ( ( 𝐺 ∈ Grp ∧ 𝐶 ∈ 𝑋 ∧ 𝐷 ∈ 𝑋 ) → ( 𝐶 + 𝐷 ) ∈ 𝑋 )
26 7 23 24 25 syl3anc ⊢ ( ( 𝑌 ∈ ( NrmSGrp ‘ 𝐺 ) ∧ ( 𝐴 ∼ 𝐶 ∧ 𝐵 ∼ 𝐷 ) ) → ( 𝐶 + 𝐷 ) ∈ 𝑋 )
27 1 3 11 grpinvadd ⊢ ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ( invg ‘ 𝐺 ) ‘ ( 𝐴 + 𝐵 ) ) = ( ( ( invg ‘ 𝐺 ) ‘ 𝐵 ) + ( ( invg ‘ 𝐺 ) ‘ 𝐴 ) ) )
28 7 15 20 27 syl3anc ⊢ ( ( 𝑌 ∈ ( NrmSGrp ‘ 𝐺 ) ∧ ( 𝐴 ∼ 𝐶 ∧ 𝐵 ∼ 𝐷 ) ) → ( ( invg ‘ 𝐺 ) ‘ ( 𝐴 + 𝐵 ) ) = ( ( ( invg ‘ 𝐺 ) ‘ 𝐵 ) + ( ( invg ‘ 𝐺 ) ‘ 𝐴 ) ) )
29 28 oveq1d ⊢ ( ( 𝑌 ∈ ( NrmSGrp ‘ 𝐺 ) ∧ ( 𝐴 ∼ 𝐶 ∧ 𝐵 ∼ 𝐷 ) ) → ( ( ( invg ‘ 𝐺 ) ‘ ( 𝐴 + 𝐵 ) ) + ( 𝐶 + 𝐷 ) ) = ( ( ( ( invg ‘ 𝐺 ) ‘ 𝐵 ) + ( ( invg ‘ 𝐺 ) ‘ 𝐴 ) ) + ( 𝐶 + 𝐷 ) ) )
30 1 11 grpinvcl ⊢ ( ( 𝐺 ∈ Grp ∧ 𝐵 ∈ 𝑋 ) → ( ( invg ‘ 𝐺 ) ‘ 𝐵 ) ∈ 𝑋 )
31 7 20 30 syl2anc ⊢ ( ( 𝑌 ∈ ( NrmSGrp ‘ 𝐺 ) ∧ ( 𝐴 ∼ 𝐶 ∧ 𝐵 ∼ 𝐷 ) ) → ( ( invg ‘ 𝐺 ) ‘ 𝐵 ) ∈ 𝑋 )
32 1 11 grpinvcl ⊢ ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ) → ( ( invg ‘ 𝐺 ) ‘ 𝐴 ) ∈ 𝑋 )
33 7 15 32 syl2anc ⊢ ( ( 𝑌 ∈ ( NrmSGrp ‘ 𝐺 ) ∧ ( 𝐴 ∼ 𝐶 ∧ 𝐵 ∼ 𝐷 ) ) → ( ( invg ‘ 𝐺 ) ‘ 𝐴 ) ∈ 𝑋 )
34 1 3 grpass ⊢ ( ( 𝐺 ∈ Grp ∧ ( ( ( invg ‘ 𝐺 ) ‘ 𝐵 ) ∈ 𝑋 ∧ ( ( invg ‘ 𝐺 ) ‘ 𝐴 ) ∈ 𝑋 ∧ ( 𝐶 + 𝐷 ) ∈ 𝑋 ) ) → ( ( ( ( invg ‘ 𝐺 ) ‘ 𝐵 ) + ( ( invg ‘ 𝐺 ) ‘ 𝐴 ) ) + ( 𝐶 + 𝐷 ) ) = ( ( ( invg ‘ 𝐺 ) ‘ 𝐵 ) + ( ( ( invg ‘ 𝐺 ) ‘ 𝐴 ) + ( 𝐶 + 𝐷 ) ) ) )
35 7 31 33 26 34 syl13anc ⊢ ( ( 𝑌 ∈ ( NrmSGrp ‘ 𝐺 ) ∧ ( 𝐴 ∼ 𝐶 ∧ 𝐵 ∼ 𝐷 ) ) → ( ( ( ( invg ‘ 𝐺 ) ‘ 𝐵 ) + ( ( invg ‘ 𝐺 ) ‘ 𝐴 ) ) + ( 𝐶 + 𝐷 ) ) = ( ( ( invg ‘ 𝐺 ) ‘ 𝐵 ) + ( ( ( invg ‘ 𝐺 ) ‘ 𝐴 ) + ( 𝐶 + 𝐷 ) ) ) )
36 29 35 eqtrd ⊢ ( ( 𝑌 ∈ ( NrmSGrp ‘ 𝐺 ) ∧ ( 𝐴 ∼ 𝐶 ∧ 𝐵 ∼ 𝐷 ) ) → ( ( ( invg ‘ 𝐺 ) ‘ ( 𝐴 + 𝐵 ) ) + ( 𝐶 + 𝐷 ) ) = ( ( ( invg ‘ 𝐺 ) ‘ 𝐵 ) + ( ( ( invg ‘ 𝐺 ) ‘ 𝐴 ) + ( 𝐶 + 𝐷 ) ) ) )
37 1 3 grpass ⊢ ( ( 𝐺 ∈ Grp ∧ ( ( ( invg ‘ 𝐺 ) ‘ 𝐴 ) ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ∧ 𝐷 ∈ 𝑋 ) ) → ( ( ( ( invg ‘ 𝐺 ) ‘ 𝐴 ) + 𝐶 ) + 𝐷 ) = ( ( ( invg ‘ 𝐺 ) ‘ 𝐴 ) + ( 𝐶 + 𝐷 ) ) )
38 7 33 23 24 37 syl13anc ⊢ ( ( 𝑌 ∈ ( NrmSGrp ‘ 𝐺 ) ∧ ( 𝐴 ∼ 𝐶 ∧ 𝐵 ∼ 𝐷 ) ) → ( ( ( ( invg ‘ 𝐺 ) ‘ 𝐴 ) + 𝐶 ) + 𝐷 ) = ( ( ( invg ‘ 𝐺 ) ‘ 𝐴 ) + ( 𝐶 + 𝐷 ) ) )
39 38 oveq1d ⊢ ( ( 𝑌 ∈ ( NrmSGrp ‘ 𝐺 ) ∧ ( 𝐴 ∼ 𝐶 ∧ 𝐵 ∼ 𝐷 ) ) → ( ( ( ( ( invg ‘ 𝐺 ) ‘ 𝐴 ) + 𝐶 ) + 𝐷 ) + ( ( invg ‘ 𝐺 ) ‘ 𝐵 ) ) = ( ( ( ( invg ‘ 𝐺 ) ‘ 𝐴 ) + ( 𝐶 + 𝐷 ) ) + ( ( invg ‘ 𝐺 ) ‘ 𝐵 ) ) )
40 1 3 grpcl ⊢ ( ( 𝐺 ∈ Grp ∧ ( ( invg ‘ 𝐺 ) ‘ 𝐴 ) ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) → ( ( ( invg ‘ 𝐺 ) ‘ 𝐴 ) + 𝐶 ) ∈ 𝑋 )
41 7 33 23 40 syl3anc ⊢ ( ( 𝑌 ∈ ( NrmSGrp ‘ 𝐺 ) ∧ ( 𝐴 ∼ 𝐶 ∧ 𝐵 ∼ 𝐷 ) ) → ( ( ( invg ‘ 𝐺 ) ‘ 𝐴 ) + 𝐶 ) ∈ 𝑋 )
42 1 3 grpass ⊢ ( ( 𝐺 ∈ Grp ∧ ( ( ( ( invg ‘ 𝐺 ) ‘ 𝐴 ) + 𝐶 ) ∈ 𝑋 ∧ 𝐷 ∈ 𝑋 ∧ ( ( invg ‘ 𝐺 ) ‘ 𝐵 ) ∈ 𝑋 ) ) → ( ( ( ( ( invg ‘ 𝐺 ) ‘ 𝐴 ) + 𝐶 ) + 𝐷 ) + ( ( invg ‘ 𝐺 ) ‘ 𝐵 ) ) = ( ( ( ( invg ‘ 𝐺 ) ‘ 𝐴 ) + 𝐶 ) + ( 𝐷 + ( ( invg ‘ 𝐺 ) ‘ 𝐵 ) ) ) )
43 7 41 24 31 42 syl13anc ⊢ ( ( 𝑌 ∈ ( NrmSGrp ‘ 𝐺 ) ∧ ( 𝐴 ∼ 𝐶 ∧ 𝐵 ∼ 𝐷 ) ) → ( ( ( ( ( invg ‘ 𝐺 ) ‘ 𝐴 ) + 𝐶 ) + 𝐷 ) + ( ( invg ‘ 𝐺 ) ‘ 𝐵 ) ) = ( ( ( ( invg ‘ 𝐺 ) ‘ 𝐴 ) + 𝐶 ) + ( 𝐷 + ( ( invg ‘ 𝐺 ) ‘ 𝐵 ) ) ) )
44 39 43 eqtr3d ⊢ ( ( 𝑌 ∈ ( NrmSGrp ‘ 𝐺 ) ∧ ( 𝐴 ∼ 𝐶 ∧ 𝐵 ∼ 𝐷 ) ) → ( ( ( ( invg ‘ 𝐺 ) ‘ 𝐴 ) + ( 𝐶 + 𝐷 ) ) + ( ( invg ‘ 𝐺 ) ‘ 𝐵 ) ) = ( ( ( ( invg ‘ 𝐺 ) ‘ 𝐴 ) + 𝐶 ) + ( 𝐷 + ( ( invg ‘ 𝐺 ) ‘ 𝐵 ) ) ) )
45 14 simp3d ⊢ ( ( 𝑌 ∈ ( NrmSGrp ‘ 𝐺 ) ∧ ( 𝐴 ∼ 𝐶 ∧ 𝐵 ∼ 𝐷 ) ) → ( ( ( invg ‘ 𝐺 ) ‘ 𝐴 ) + 𝐶 ) ∈ 𝑌 )
46 19 simp3d ⊢ ( ( 𝑌 ∈ ( NrmSGrp ‘ 𝐺 ) ∧ ( 𝐴 ∼ 𝐶 ∧ 𝐵 ∼ 𝐷 ) ) → ( ( ( invg ‘ 𝐺 ) ‘ 𝐵 ) + 𝐷 ) ∈ 𝑌 )
47 simpl ⊢ ( ( 𝑌 ∈ ( NrmSGrp ‘ 𝐺 ) ∧ ( 𝐴 ∼ 𝐶 ∧ 𝐵 ∼ 𝐷 ) ) → 𝑌 ∈ ( NrmSGrp ‘ 𝐺 ) )
48 1 3 nsgbi ⊢ ( ( 𝑌 ∈ ( NrmSGrp ‘ 𝐺 ) ∧ ( ( invg ‘ 𝐺 ) ‘ 𝐵 ) ∈ 𝑋 ∧ 𝐷 ∈ 𝑋 ) → ( ( ( ( invg ‘ 𝐺 ) ‘ 𝐵 ) + 𝐷 ) ∈ 𝑌 ↔ ( 𝐷 + ( ( invg ‘ 𝐺 ) ‘ 𝐵 ) ) ∈ 𝑌 ) )
49 47 31 24 48 syl3anc ⊢ ( ( 𝑌 ∈ ( NrmSGrp ‘ 𝐺 ) ∧ ( 𝐴 ∼ 𝐶 ∧ 𝐵 ∼ 𝐷 ) ) → ( ( ( ( invg ‘ 𝐺 ) ‘ 𝐵 ) + 𝐷 ) ∈ 𝑌 ↔ ( 𝐷 + ( ( invg ‘ 𝐺 ) ‘ 𝐵 ) ) ∈ 𝑌 ) )
50 46 49 mpbid ⊢ ( ( 𝑌 ∈ ( NrmSGrp ‘ 𝐺 ) ∧ ( 𝐴 ∼ 𝐶 ∧ 𝐵 ∼ 𝐷 ) ) → ( 𝐷 + ( ( invg ‘ 𝐺 ) ‘ 𝐵 ) ) ∈ 𝑌 )
51 3 subgcl ⊢ ( ( 𝑌 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( ( ( invg ‘ 𝐺 ) ‘ 𝐴 ) + 𝐶 ) ∈ 𝑌 ∧ ( 𝐷 + ( ( invg ‘ 𝐺 ) ‘ 𝐵 ) ) ∈ 𝑌 ) → ( ( ( ( invg ‘ 𝐺 ) ‘ 𝐴 ) + 𝐶 ) + ( 𝐷 + ( ( invg ‘ 𝐺 ) ‘ 𝐵 ) ) ) ∈ 𝑌 )
52 5 45 50 51 syl3anc ⊢ ( ( 𝑌 ∈ ( NrmSGrp ‘ 𝐺 ) ∧ ( 𝐴 ∼ 𝐶 ∧ 𝐵 ∼ 𝐷 ) ) → ( ( ( ( invg ‘ 𝐺 ) ‘ 𝐴 ) + 𝐶 ) + ( 𝐷 + ( ( invg ‘ 𝐺 ) ‘ 𝐵 ) ) ) ∈ 𝑌 )
53 44 52 eqeltrd ⊢ ( ( 𝑌 ∈ ( NrmSGrp ‘ 𝐺 ) ∧ ( 𝐴 ∼ 𝐶 ∧ 𝐵 ∼ 𝐷 ) ) → ( ( ( ( invg ‘ 𝐺 ) ‘ 𝐴 ) + ( 𝐶 + 𝐷 ) ) + ( ( invg ‘ 𝐺 ) ‘ 𝐵 ) ) ∈ 𝑌 )
54 1 3 grpcl ⊢ ( ( 𝐺 ∈ Grp ∧ ( ( invg ‘ 𝐺 ) ‘ 𝐴 ) ∈ 𝑋 ∧ ( 𝐶 + 𝐷 ) ∈ 𝑋 ) → ( ( ( invg ‘ 𝐺 ) ‘ 𝐴 ) + ( 𝐶 + 𝐷 ) ) ∈ 𝑋 )
55 7 33 26 54 syl3anc ⊢ ( ( 𝑌 ∈ ( NrmSGrp ‘ 𝐺 ) ∧ ( 𝐴 ∼ 𝐶 ∧ 𝐵 ∼ 𝐷 ) ) → ( ( ( invg ‘ 𝐺 ) ‘ 𝐴 ) + ( 𝐶 + 𝐷 ) ) ∈ 𝑋 )
56 1 3 nsgbi ⊢ ( ( 𝑌 ∈ ( NrmSGrp ‘ 𝐺 ) ∧ ( ( ( invg ‘ 𝐺 ) ‘ 𝐴 ) + ( 𝐶 + 𝐷 ) ) ∈ 𝑋 ∧ ( ( invg ‘ 𝐺 ) ‘ 𝐵 ) ∈ 𝑋 ) → ( ( ( ( ( invg ‘ 𝐺 ) ‘ 𝐴 ) + ( 𝐶 + 𝐷 ) ) + ( ( invg ‘ 𝐺 ) ‘ 𝐵 ) ) ∈ 𝑌 ↔ ( ( ( invg ‘ 𝐺 ) ‘ 𝐵 ) + ( ( ( invg ‘ 𝐺 ) ‘ 𝐴 ) + ( 𝐶 + 𝐷 ) ) ) ∈ 𝑌 ) )
57 47 55 31 56 syl3anc ⊢ ( ( 𝑌 ∈ ( NrmSGrp ‘ 𝐺 ) ∧ ( 𝐴 ∼ 𝐶 ∧ 𝐵 ∼ 𝐷 ) ) → ( ( ( ( ( invg ‘ 𝐺 ) ‘ 𝐴 ) + ( 𝐶 + 𝐷 ) ) + ( ( invg ‘ 𝐺 ) ‘ 𝐵 ) ) ∈ 𝑌 ↔ ( ( ( invg ‘ 𝐺 ) ‘ 𝐵 ) + ( ( ( invg ‘ 𝐺 ) ‘ 𝐴 ) + ( 𝐶 + 𝐷 ) ) ) ∈ 𝑌 ) )
58 53 57 mpbid ⊢ ( ( 𝑌 ∈ ( NrmSGrp ‘ 𝐺 ) ∧ ( 𝐴 ∼ 𝐶 ∧ 𝐵 ∼ 𝐷 ) ) → ( ( ( invg ‘ 𝐺 ) ‘ 𝐵 ) + ( ( ( invg ‘ 𝐺 ) ‘ 𝐴 ) + ( 𝐶 + 𝐷 ) ) ) ∈ 𝑌 )
59 36 58 eqeltrd ⊢ ( ( 𝑌 ∈ ( NrmSGrp ‘ 𝐺 ) ∧ ( 𝐴 ∼ 𝐶 ∧ 𝐵 ∼ 𝐷 ) ) → ( ( ( invg ‘ 𝐺 ) ‘ ( 𝐴 + 𝐵 ) ) + ( 𝐶 + 𝐷 ) ) ∈ 𝑌 )
60 1 11 3 2 eqgval ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑌 ⊆ 𝑋 ) → ( ( 𝐴 + 𝐵 ) ∼ ( 𝐶 + 𝐷 ) ↔ ( ( 𝐴 + 𝐵 ) ∈ 𝑋 ∧ ( 𝐶 + 𝐷 ) ∈ 𝑋 ∧ ( ( ( invg ‘ 𝐺 ) ‘ ( 𝐴 + 𝐵 ) ) + ( 𝐶 + 𝐷 ) ) ∈ 𝑌 ) ) )
61 7 10 60 syl2anc ⊢ ( ( 𝑌 ∈ ( NrmSGrp ‘ 𝐺 ) ∧ ( 𝐴 ∼ 𝐶 ∧ 𝐵 ∼ 𝐷 ) ) → ( ( 𝐴 + 𝐵 ) ∼ ( 𝐶 + 𝐷 ) ↔ ( ( 𝐴 + 𝐵 ) ∈ 𝑋 ∧ ( 𝐶 + 𝐷 ) ∈ 𝑋 ∧ ( ( ( invg ‘ 𝐺 ) ‘ ( 𝐴 + 𝐵 ) ) + ( 𝐶 + 𝐷 ) ) ∈ 𝑌 ) ) )
62 22 26 59 61 mpbir3and ⊢ ( ( 𝑌 ∈ ( NrmSGrp ‘ 𝐺 ) ∧ ( 𝐴 ∼ 𝐶 ∧ 𝐵 ∼ 𝐷 ) ) → ( 𝐴 + 𝐵 ) ∼ ( 𝐶 + 𝐷 ) )
63 62 ex ⊢ ( 𝑌 ∈ ( NrmSGrp ‘ 𝐺 ) → ( ( 𝐴 ∼ 𝐶 ∧ 𝐵 ∼ 𝐷 ) → ( 𝐴 + 𝐵 ) ∼ ( 𝐶 + 𝐷 ) ) )