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 
|- X = ( Base ` G )
eqger.r 
|- .~ = ( G ~QG Y )
eqgcpbl.p 
|- .+ = ( +g ` G )
Assertion eqgcpbl 
|- ( Y e. ( NrmSGrp ` G ) -> ( ( A .~ C /\ B .~ D ) -> ( A .+ B ) .~ ( C .+ D ) ) )

Proof

Step Hyp Ref Expression
1 eqger.x 
 |-  X = ( Base ` G )
2 eqger.r 
 |-  .~ = ( G ~QG Y )
3 eqgcpbl.p 
 |-  .+ = ( +g ` G )
4 nsgsubg 
 |-  ( Y e. ( NrmSGrp ` G ) -> Y e. ( SubGrp ` G ) )
5 4 adantr 
 |-  ( ( Y e. ( NrmSGrp ` G ) /\ ( A .~ C /\ B .~ D ) ) -> Y e. ( SubGrp ` G ) )
6 subgrcl 
 |-  ( Y e. ( SubGrp ` G ) -> G e. Grp )
7 5 6 syl 
 |-  ( ( Y e. ( NrmSGrp ` G ) /\ ( A .~ C /\ B .~ D ) ) -> G e. Grp )
8 simprl 
 |-  ( ( Y e. ( NrmSGrp ` G ) /\ ( A .~ C /\ B .~ D ) ) -> A .~ C )
9 1 subgss 
 |-  ( Y e. ( SubGrp ` G ) -> Y C_ X )
10 5 9 syl 
 |-  ( ( Y e. ( NrmSGrp ` G ) /\ ( A .~ C /\ B .~ D ) ) -> Y C_ X )
11 eqid 
 |-  ( invg ` G ) = ( invg ` G )
12 1 11 3 2 eqgval 
 |-  ( ( G e. Grp /\ Y C_ X ) -> ( A .~ C <-> ( A e. X /\ C e. X /\ ( ( ( invg ` G ) ` A ) .+ C ) e. Y ) ) )
13 7 10 12 syl2anc 
 |-  ( ( Y e. ( NrmSGrp ` G ) /\ ( A .~ C /\ B .~ D ) ) -> ( A .~ C <-> ( A e. X /\ C e. X /\ ( ( ( invg ` G ) ` A ) .+ C ) e. Y ) ) )
14 8 13 mpbid 
 |-  ( ( Y e. ( NrmSGrp ` G ) /\ ( A .~ C /\ B .~ D ) ) -> ( A e. X /\ C e. X /\ ( ( ( invg ` G ) ` A ) .+ C ) e. Y ) )
15 14 simp1d 
 |-  ( ( Y e. ( NrmSGrp ` G ) /\ ( A .~ C /\ B .~ D ) ) -> A e. X )
16 simprr 
 |-  ( ( Y e. ( NrmSGrp ` G ) /\ ( A .~ C /\ B .~ D ) ) -> B .~ D )
17 1 11 3 2 eqgval 
 |-  ( ( G e. Grp /\ Y C_ X ) -> ( B .~ D <-> ( B e. X /\ D e. X /\ ( ( ( invg ` G ) ` B ) .+ D ) e. Y ) ) )
18 7 10 17 syl2anc 
 |-  ( ( Y e. ( NrmSGrp ` G ) /\ ( A .~ C /\ B .~ D ) ) -> ( B .~ D <-> ( B e. X /\ D e. X /\ ( ( ( invg ` G ) ` B ) .+ D ) e. Y ) ) )
19 16 18 mpbid 
 |-  ( ( Y e. ( NrmSGrp ` G ) /\ ( A .~ C /\ B .~ D ) ) -> ( B e. X /\ D e. X /\ ( ( ( invg ` G ) ` B ) .+ D ) e. Y ) )
20 19 simp1d 
 |-  ( ( Y e. ( NrmSGrp ` G ) /\ ( A .~ C /\ B .~ D ) ) -> B e. X )
21 1 3 grpcl 
 |-  ( ( G e. Grp /\ A e. X /\ B e. X ) -> ( A .+ B ) e. X )
22 7 15 20 21 syl3anc 
 |-  ( ( Y e. ( NrmSGrp ` G ) /\ ( A .~ C /\ B .~ D ) ) -> ( A .+ B ) e. X )
23 14 simp2d 
 |-  ( ( Y e. ( NrmSGrp ` G ) /\ ( A .~ C /\ B .~ D ) ) -> C e. X )
24 19 simp2d 
 |-  ( ( Y e. ( NrmSGrp ` G ) /\ ( A .~ C /\ B .~ D ) ) -> D e. X )
25 1 3 grpcl 
 |-  ( ( G e. Grp /\ C e. X /\ D e. X ) -> ( C .+ D ) e. X )
26 7 23 24 25 syl3anc 
 |-  ( ( Y e. ( NrmSGrp ` G ) /\ ( A .~ C /\ B .~ D ) ) -> ( C .+ D ) e. X )
27 1 3 11 grpinvadd 
 |-  ( ( G e. Grp /\ A e. X /\ B e. X ) -> ( ( invg ` G ) ` ( A .+ B ) ) = ( ( ( invg ` G ) ` B ) .+ ( ( invg ` G ) ` A ) ) )
28 7 15 20 27 syl3anc 
 |-  ( ( Y e. ( NrmSGrp ` G ) /\ ( A .~ C /\ B .~ D ) ) -> ( ( invg ` G ) ` ( A .+ B ) ) = ( ( ( invg ` G ) ` B ) .+ ( ( invg ` G ) ` A ) ) )
29 28 oveq1d 
 |-  ( ( Y e. ( NrmSGrp ` G ) /\ ( A .~ C /\ B .~ D ) ) -> ( ( ( invg ` G ) ` ( A .+ B ) ) .+ ( C .+ D ) ) = ( ( ( ( invg ` G ) ` B ) .+ ( ( invg ` G ) ` A ) ) .+ ( C .+ D ) ) )
30 1 11 grpinvcl 
 |-  ( ( G e. Grp /\ B e. X ) -> ( ( invg ` G ) ` B ) e. X )
31 7 20 30 syl2anc 
 |-  ( ( Y e. ( NrmSGrp ` G ) /\ ( A .~ C /\ B .~ D ) ) -> ( ( invg ` G ) ` B ) e. X )
32 1 11 grpinvcl 
 |-  ( ( G e. Grp /\ A e. X ) -> ( ( invg ` G ) ` A ) e. X )
33 7 15 32 syl2anc 
 |-  ( ( Y e. ( NrmSGrp ` G ) /\ ( A .~ C /\ B .~ D ) ) -> ( ( invg ` G ) ` A ) e. X )
34 1 3 grpass 
 |-  ( ( G e. Grp /\ ( ( ( invg ` G ) ` B ) e. X /\ ( ( invg ` G ) ` A ) e. X /\ ( C .+ D ) e. X ) ) -> ( ( ( ( invg ` G ) ` B ) .+ ( ( invg ` G ) ` A ) ) .+ ( C .+ D ) ) = ( ( ( invg ` G ) ` B ) .+ ( ( ( invg ` G ) ` A ) .+ ( C .+ D ) ) ) )
35 7 31 33 26 34 syl13anc 
 |-  ( ( Y e. ( NrmSGrp ` G ) /\ ( A .~ C /\ B .~ D ) ) -> ( ( ( ( invg ` G ) ` B ) .+ ( ( invg ` G ) ` A ) ) .+ ( C .+ D ) ) = ( ( ( invg ` G ) ` B ) .+ ( ( ( invg ` G ) ` A ) .+ ( C .+ D ) ) ) )
36 29 35 eqtrd 
 |-  ( ( Y e. ( NrmSGrp ` G ) /\ ( A .~ C /\ B .~ D ) ) -> ( ( ( invg ` G ) ` ( A .+ B ) ) .+ ( C .+ D ) ) = ( ( ( invg ` G ) ` B ) .+ ( ( ( invg ` G ) ` A ) .+ ( C .+ D ) ) ) )
37 1 3 grpass 
 |-  ( ( G e. Grp /\ ( ( ( invg ` G ) ` A ) e. X /\ C e. X /\ D e. X ) ) -> ( ( ( ( invg ` G ) ` A ) .+ C ) .+ D ) = ( ( ( invg ` G ) ` A ) .+ ( C .+ D ) ) )
38 7 33 23 24 37 syl13anc 
 |-  ( ( Y e. ( NrmSGrp ` G ) /\ ( A .~ C /\ B .~ D ) ) -> ( ( ( ( invg ` G ) ` A ) .+ C ) .+ D ) = ( ( ( invg ` G ) ` A ) .+ ( C .+ D ) ) )
39 38 oveq1d 
 |-  ( ( Y e. ( NrmSGrp ` G ) /\ ( A .~ C /\ B .~ D ) ) -> ( ( ( ( ( invg ` G ) ` A ) .+ C ) .+ D ) .+ ( ( invg ` G ) ` B ) ) = ( ( ( ( invg ` G ) ` A ) .+ ( C .+ D ) ) .+ ( ( invg ` G ) ` B ) ) )
40 1 3 grpcl 
 |-  ( ( G e. Grp /\ ( ( invg ` G ) ` A ) e. X /\ C e. X ) -> ( ( ( invg ` G ) ` A ) .+ C ) e. X )
41 7 33 23 40 syl3anc 
 |-  ( ( Y e. ( NrmSGrp ` G ) /\ ( A .~ C /\ B .~ D ) ) -> ( ( ( invg ` G ) ` A ) .+ C ) e. X )
42 1 3 grpass 
 |-  ( ( G e. Grp /\ ( ( ( ( invg ` G ) ` A ) .+ C ) e. X /\ D e. X /\ ( ( invg ` G ) ` B ) e. X ) ) -> ( ( ( ( ( invg ` G ) ` A ) .+ C ) .+ D ) .+ ( ( invg ` G ) ` B ) ) = ( ( ( ( invg ` G ) ` A ) .+ C ) .+ ( D .+ ( ( invg ` G ) ` B ) ) ) )
43 7 41 24 31 42 syl13anc 
 |-  ( ( Y e. ( NrmSGrp ` G ) /\ ( A .~ C /\ B .~ D ) ) -> ( ( ( ( ( invg ` G ) ` A ) .+ C ) .+ D ) .+ ( ( invg ` G ) ` B ) ) = ( ( ( ( invg ` G ) ` A ) .+ C ) .+ ( D .+ ( ( invg ` G ) ` B ) ) ) )
44 39 43 eqtr3d 
 |-  ( ( Y e. ( NrmSGrp ` G ) /\ ( A .~ C /\ B .~ D ) ) -> ( ( ( ( invg ` G ) ` A ) .+ ( C .+ D ) ) .+ ( ( invg ` G ) ` B ) ) = ( ( ( ( invg ` G ) ` A ) .+ C ) .+ ( D .+ ( ( invg ` G ) ` B ) ) ) )
45 14 simp3d 
 |-  ( ( Y e. ( NrmSGrp ` G ) /\ ( A .~ C /\ B .~ D ) ) -> ( ( ( invg ` G ) ` A ) .+ C ) e. Y )
46 19 simp3d 
 |-  ( ( Y e. ( NrmSGrp ` G ) /\ ( A .~ C /\ B .~ D ) ) -> ( ( ( invg ` G ) ` B ) .+ D ) e. Y )
47 simpl 
 |-  ( ( Y e. ( NrmSGrp ` G ) /\ ( A .~ C /\ B .~ D ) ) -> Y e. ( NrmSGrp ` G ) )
48 1 3 nsgbi 
 |-  ( ( Y e. ( NrmSGrp ` G ) /\ ( ( invg ` G ) ` B ) e. X /\ D e. X ) -> ( ( ( ( invg ` G ) ` B ) .+ D ) e. Y <-> ( D .+ ( ( invg ` G ) ` B ) ) e. Y ) )
49 47 31 24 48 syl3anc 
 |-  ( ( Y e. ( NrmSGrp ` G ) /\ ( A .~ C /\ B .~ D ) ) -> ( ( ( ( invg ` G ) ` B ) .+ D ) e. Y <-> ( D .+ ( ( invg ` G ) ` B ) ) e. Y ) )
50 46 49 mpbid 
 |-  ( ( Y e. ( NrmSGrp ` G ) /\ ( A .~ C /\ B .~ D ) ) -> ( D .+ ( ( invg ` G ) ` B ) ) e. Y )
51 3 subgcl 
 |-  ( ( Y e. ( SubGrp ` G ) /\ ( ( ( invg ` G ) ` A ) .+ C ) e. Y /\ ( D .+ ( ( invg ` G ) ` B ) ) e. Y ) -> ( ( ( ( invg ` G ) ` A ) .+ C ) .+ ( D .+ ( ( invg ` G ) ` B ) ) ) e. Y )
52 5 45 50 51 syl3anc 
 |-  ( ( Y e. ( NrmSGrp ` G ) /\ ( A .~ C /\ B .~ D ) ) -> ( ( ( ( invg ` G ) ` A ) .+ C ) .+ ( D .+ ( ( invg ` G ) ` B ) ) ) e. Y )
53 44 52 eqeltrd 
 |-  ( ( Y e. ( NrmSGrp ` G ) /\ ( A .~ C /\ B .~ D ) ) -> ( ( ( ( invg ` G ) ` A ) .+ ( C .+ D ) ) .+ ( ( invg ` G ) ` B ) ) e. Y )
54 1 3 grpcl 
 |-  ( ( G e. Grp /\ ( ( invg ` G ) ` A ) e. X /\ ( C .+ D ) e. X ) -> ( ( ( invg ` G ) ` A ) .+ ( C .+ D ) ) e. X )
55 7 33 26 54 syl3anc 
 |-  ( ( Y e. ( NrmSGrp ` G ) /\ ( A .~ C /\ B .~ D ) ) -> ( ( ( invg ` G ) ` A ) .+ ( C .+ D ) ) e. X )
56 1 3 nsgbi 
 |-  ( ( Y e. ( NrmSGrp ` G ) /\ ( ( ( invg ` G ) ` A ) .+ ( C .+ D ) ) e. X /\ ( ( invg ` G ) ` B ) e. X ) -> ( ( ( ( ( invg ` G ) ` A ) .+ ( C .+ D ) ) .+ ( ( invg ` G ) ` B ) ) e. Y <-> ( ( ( invg ` G ) ` B ) .+ ( ( ( invg ` G ) ` A ) .+ ( C .+ D ) ) ) e. Y ) )
57 47 55 31 56 syl3anc 
 |-  ( ( Y e. ( NrmSGrp ` G ) /\ ( A .~ C /\ B .~ D ) ) -> ( ( ( ( ( invg ` G ) ` A ) .+ ( C .+ D ) ) .+ ( ( invg ` G ) ` B ) ) e. Y <-> ( ( ( invg ` G ) ` B ) .+ ( ( ( invg ` G ) ` A ) .+ ( C .+ D ) ) ) e. Y ) )
58 53 57 mpbid 
 |-  ( ( Y e. ( NrmSGrp ` G ) /\ ( A .~ C /\ B .~ D ) ) -> ( ( ( invg ` G ) ` B ) .+ ( ( ( invg ` G ) ` A ) .+ ( C .+ D ) ) ) e. Y )
59 36 58 eqeltrd 
 |-  ( ( Y e. ( NrmSGrp ` G ) /\ ( A .~ C /\ B .~ D ) ) -> ( ( ( invg ` G ) ` ( A .+ B ) ) .+ ( C .+ D ) ) e. Y )
60 1 11 3 2 eqgval 
 |-  ( ( G e. Grp /\ Y C_ X ) -> ( ( A .+ B ) .~ ( C .+ D ) <-> ( ( A .+ B ) e. X /\ ( C .+ D ) e. X /\ ( ( ( invg ` G ) ` ( A .+ B ) ) .+ ( C .+ D ) ) e. Y ) ) )
61 7 10 60 syl2anc 
 |-  ( ( Y e. ( NrmSGrp ` G ) /\ ( A .~ C /\ B .~ D ) ) -> ( ( A .+ B ) .~ ( C .+ D ) <-> ( ( A .+ B ) e. X /\ ( C .+ D ) e. X /\ ( ( ( invg ` G ) ` ( A .+ B ) ) .+ ( C .+ D ) ) e. Y ) ) )
62 22 26 59 61 mpbir3and 
 |-  ( ( Y e. ( NrmSGrp ` G ) /\ ( A .~ C /\ B .~ D ) ) -> ( A .+ B ) .~ ( C .+ D ) )
63 62 ex 
 |-  ( Y e. ( NrmSGrp ` G ) -> ( ( A .~ C /\ B .~ D ) -> ( A .+ B ) .~ ( C .+ D ) ) )