Metamath Proof Explorer

Theorem qus0subgadd

Description: The addition in a quotient of a group by the trivial (zero) subgroup. (Contributed by AV, 26-Feb-2025)

Ref Expression
Hypotheses qus0subg.0 
|- .0. = ( 0g ` G )
qus0subg.s 
|- S = { .0. }
qus0subg.e 
|- .~ = ( G ~QG S )
qus0subg.u 
|- U = ( G /s .~ )
qus0subg.b 
|- B = ( Base ` G )
Assertion qus0subgadd 
|- ( G e. Grp -> A. a e. B A. b e. B ( { a } ( +g ` U ) { b } ) = { ( a ( +g ` G ) b ) } )

Proof

Step Hyp Ref Expression
1 qus0subg.0 
 |-  .0. = ( 0g ` G )
2 qus0subg.s 
 |-  S = { .0. }
3 qus0subg.e 
 |-  .~ = ( G ~QG S )
4 qus0subg.u 
 |-  U = ( G /s .~ )
5 qus0subg.b 
 |-  B = ( Base ` G )
6 4 a1i 
 |-  ( G e. Grp -> U = ( G /s .~ ) )
7 5 a1i 
 |-  ( G e. Grp -> B = ( Base ` G ) )
8 1 0subg 
 |-  ( G e. Grp -> { .0. } e. ( SubGrp ` G ) )
9 2 8 eqeltrid 
 |-  ( G e. Grp -> S e. ( SubGrp ` G ) )
10 5 3 eqger 
 |-  ( S e. ( SubGrp ` G ) -> .~ Er B )
11 9 10 syl 
 |-  ( G e. Grp -> .~ Er B )
12 id 
 |-  ( G e. Grp -> G e. Grp )
13 1 0nsg 
 |-  ( G e. Grp -> { .0. } e. ( NrmSGrp ` G ) )
14 2 13 eqeltrid 
 |-  ( G e. Grp -> S e. ( NrmSGrp ` G ) )
15 eqid 
 |-  ( +g ` G ) = ( +g ` G )
16 5 3 15 eqgcpbl 
 |-  ( S e. ( NrmSGrp ` G ) -> ( ( x .~ p /\ y .~ q ) -> ( x ( +g ` G ) y ) .~ ( p ( +g ` G ) q ) ) )
17 14 16 syl 
 |-  ( G e. Grp -> ( ( x .~ p /\ y .~ q ) -> ( x ( +g ` G ) y ) .~ ( p ( +g ` G ) q ) ) )
18 5 15 grpcl 
 |-  ( ( G e. Grp /\ p e. B /\ q e. B ) -> ( p ( +g ` G ) q ) e. B )
19 18 3expb 
 |-  ( ( G e. Grp /\ ( p e. B /\ q e. B ) ) -> ( p ( +g ` G ) q ) e. B )
20 eqid 
 |-  ( +g ` U ) = ( +g ` U )
21 6 7 11 12 17 19 15 20 qusaddval 
 |-  ( ( G e. Grp /\ a e. B /\ b e. B ) -> ( [ a ] .~ ( +g ` U ) [ b ] .~ ) = [ ( a ( +g ` G ) b ) ] .~ )
22 21 3expb 
 |-  ( ( G e. Grp /\ ( a e. B /\ b e. B ) ) -> ( [ a ] .~ ( +g ` U ) [ b ] .~ ) = [ ( a ( +g ` G ) b ) ] .~ )
23 1 2 5 3 eqg0subgecsn 
 |-  ( ( G e. Grp /\ a e. B ) -> [ a ] .~ = { a } )
24 23 adantrr 
 |-  ( ( G e. Grp /\ ( a e. B /\ b e. B ) ) -> [ a ] .~ = { a } )
25 1 2 5 3 eqg0subgecsn 
 |-  ( ( G e. Grp /\ b e. B ) -> [ b ] .~ = { b } )
26 25 adantrl 
 |-  ( ( G e. Grp /\ ( a e. B /\ b e. B ) ) -> [ b ] .~ = { b } )
27 24 26 oveq12d 
 |-  ( ( G e. Grp /\ ( a e. B /\ b e. B ) ) -> ( [ a ] .~ ( +g ` U ) [ b ] .~ ) = ( { a } ( +g ` U ) { b } ) )
28 5 15 grpcl 
 |-  ( ( G e. Grp /\ a e. B /\ b e. B ) -> ( a ( +g ` G ) b ) e. B )
29 28 3expb 
 |-  ( ( G e. Grp /\ ( a e. B /\ b e. B ) ) -> ( a ( +g ` G ) b ) e. B )
30 1 2 5 3 eqg0subgecsn 
 |-  ( ( G e. Grp /\ ( a ( +g ` G ) b ) e. B ) -> [ ( a ( +g ` G ) b ) ] .~ = { ( a ( +g ` G ) b ) } )
31 29 30 syldan 
 |-  ( ( G e. Grp /\ ( a e. B /\ b e. B ) ) -> [ ( a ( +g ` G ) b ) ] .~ = { ( a ( +g ` G ) b ) } )
32 22 27 31 3eqtr3d 
 |-  ( ( G e. Grp /\ ( a e. B /\ b e. B ) ) -> ( { a } ( +g ` U ) { b } ) = { ( a ( +g ` G ) b ) } )
33 32 ralrimivva 
 |-  ( G e. Grp -> A. a e. B A. b e. B ( { a } ( +g ` U ) { b } ) = { ( a ( +g ` G ) b ) } )