Metamath Proof Explorer

Theorem quslsm

Description: Express the image by the quotient map in terms of direct sum. (Contributed by Thierry Arnoux, 27-Jul-2024)

Ref Expression
Hypotheses quslsm.b 
|- B = ( Base ` G )
quslsm.p 
|- .(+) = ( LSSum ` G )
quslsm.n 
|- ( ph -> S e. ( SubGrp ` G ) )
quslsm.s 
|- ( ph -> X e. B )
Assertion quslsm 
|- ( ph -> [ X ] ( G ~QG S ) = ( { X } .(+) S ) )

Proof

Step Hyp Ref Expression
1 quslsm.b 
 |-  B = ( Base ` G )
2 quslsm.p 
 |-  .(+) = ( LSSum ` G )
3 quslsm.n 
 |-  ( ph -> S e. ( SubGrp ` G ) )
4 quslsm.s 
 |-  ( ph -> X e. B )
5 subgrcl 
 |-  ( S e. ( SubGrp ` G ) -> G e. Grp )
6 3 5 syl 
 |-  ( ph -> G e. Grp )
7 1 subgss 
 |-  ( S e. ( SubGrp ` G ) -> S C_ B )
8 3 7 syl 
 |-  ( ph -> S C_ B )
9 eqid 
 |-  ( invg ` G ) = ( invg ` G )
10 eqid 
 |-  ( +g ` G ) = ( +g ` G )
11 eqid 
 |-  ( G ~QG S ) = ( G ~QG S )
12 1 9 10 11 eqgfval 
 |-  ( ( G e. Grp /\ S C_ B ) -> ( G ~QG S ) = { <. i , j >. | ( { i , j } C_ B /\ ( ( ( invg ` G ) ` i ) ( +g ` G ) j ) e. S ) } )
13 6 8 12 syl2anc 
 |-  ( ph -> ( G ~QG S ) = { <. i , j >. | ( { i , j } C_ B /\ ( ( ( invg ` G ) ` i ) ( +g ` G ) j ) e. S ) } )
14 simpr 
 |-  ( ( ( ph /\ { i , j } C_ B ) /\ ( ( ( invg ` G ) ` i ) ( +g ` G ) j ) e. S ) -> ( ( ( invg ` G ) ` i ) ( +g ` G ) j ) e. S )
15 oveq2 
 |-  ( k = ( ( ( invg ` G ) ` i ) ( +g ` G ) j ) -> ( i ( +g ` G ) k ) = ( i ( +g ` G ) ( ( ( invg ` G ) ` i ) ( +g ` G ) j ) ) )
16 15 eqeq1d 
 |-  ( k = ( ( ( invg ` G ) ` i ) ( +g ` G ) j ) -> ( ( i ( +g ` G ) k ) = j <-> ( i ( +g ` G ) ( ( ( invg ` G ) ` i ) ( +g ` G ) j ) ) = j ) )
17 16 adantl 
 |-  ( ( ( ( ph /\ { i , j } C_ B ) /\ ( ( ( invg ` G ) ` i ) ( +g ` G ) j ) e. S ) /\ k = ( ( ( invg ` G ) ` i ) ( +g ` G ) j ) ) -> ( ( i ( +g ` G ) k ) = j <-> ( i ( +g ` G ) ( ( ( invg ` G ) ` i ) ( +g ` G ) j ) ) = j ) )
18 6 adantr 
 |-  ( ( ph /\ { i , j } C_ B ) -> G e. Grp )
19 vex 
 |-  i e. _V
20 vex 
 |-  j e. _V
21 19 20 prss 
 |-  ( ( i e. B /\ j e. B ) <-> { i , j } C_ B )
22 21 bicomi 
 |-  ( { i , j } C_ B <-> ( i e. B /\ j e. B ) )
23 22 simplbi 
 |-  ( { i , j } C_ B -> i e. B )
24 23 adantl 
 |-  ( ( ph /\ { i , j } C_ B ) -> i e. B )
25 eqid 
 |-  ( 0g ` G ) = ( 0g ` G )
26 1 10 25 9 grprinv 
 |-  ( ( G e. Grp /\ i e. B ) -> ( i ( +g ` G ) ( ( invg ` G ) ` i ) ) = ( 0g ` G ) )
27 18 24 26 syl2anc 
 |-  ( ( ph /\ { i , j } C_ B ) -> ( i ( +g ` G ) ( ( invg ` G ) ` i ) ) = ( 0g ` G ) )
28 27 oveq1d 
 |-  ( ( ph /\ { i , j } C_ B ) -> ( ( i ( +g ` G ) ( ( invg ` G ) ` i ) ) ( +g ` G ) j ) = ( ( 0g ` G ) ( +g ` G ) j ) )
29 1 9 grpinvcl 
 |-  ( ( G e. Grp /\ i e. B ) -> ( ( invg ` G ) ` i ) e. B )
30 18 24 29 syl2anc 
 |-  ( ( ph /\ { i , j } C_ B ) -> ( ( invg ` G ) ` i ) e. B )
31 22 simprbi 
 |-  ( { i , j } C_ B -> j e. B )
32 31 adantl 
 |-  ( ( ph /\ { i , j } C_ B ) -> j e. B )
33 1 10 grpass 
 |-  ( ( G e. Grp /\ ( i e. B /\ ( ( invg ` G ) ` i ) e. B /\ j e. B ) ) -> ( ( i ( +g ` G ) ( ( invg ` G ) ` i ) ) ( +g ` G ) j ) = ( i ( +g ` G ) ( ( ( invg ` G ) ` i ) ( +g ` G ) j ) ) )
34 18 24 30 32 33 syl13anc 
 |-  ( ( ph /\ { i , j } C_ B ) -> ( ( i ( +g ` G ) ( ( invg ` G ) ` i ) ) ( +g ` G ) j ) = ( i ( +g ` G ) ( ( ( invg ` G ) ` i ) ( +g ` G ) j ) ) )
35 1 10 25 grplid 
 |-  ( ( G e. Grp /\ j e. B ) -> ( ( 0g ` G ) ( +g ` G ) j ) = j )
36 18 32 35 syl2anc 
 |-  ( ( ph /\ { i , j } C_ B ) -> ( ( 0g ` G ) ( +g ` G ) j ) = j )
37 28 34 36 3eqtr3d 
 |-  ( ( ph /\ { i , j } C_ B ) -> ( i ( +g ` G ) ( ( ( invg ` G ) ` i ) ( +g ` G ) j ) ) = j )
38 37 adantr 
 |-  ( ( ( ph /\ { i , j } C_ B ) /\ ( ( ( invg ` G ) ` i ) ( +g ` G ) j ) e. S ) -> ( i ( +g ` G ) ( ( ( invg ` G ) ` i ) ( +g ` G ) j ) ) = j )
39 14 17 38 rspcedvd 
 |-  ( ( ( ph /\ { i , j } C_ B ) /\ ( ( ( invg ` G ) ` i ) ( +g ` G ) j ) e. S ) -> E. k e. S ( i ( +g ` G ) k ) = j )
40 oveq2 
 |-  ( ( i ( +g ` G ) k ) = j -> ( ( ( invg ` G ) ` i ) ( +g ` G ) ( i ( +g ` G ) k ) ) = ( ( ( invg ` G ) ` i ) ( +g ` G ) j ) )
41 40 adantl 
 |-  ( ( ( ( ph /\ { i , j } C_ B ) /\ k e. S ) /\ ( i ( +g ` G ) k ) = j ) -> ( ( ( invg ` G ) ` i ) ( +g ` G ) ( i ( +g ` G ) k ) ) = ( ( ( invg ` G ) ` i ) ( +g ` G ) j ) )
42 simpll 
 |-  ( ( ( ph /\ { i , j } C_ B ) /\ k e. S ) -> ph )
43 24 adantr 
 |-  ( ( ( ph /\ { i , j } C_ B ) /\ k e. S ) -> i e. B )
44 8 adantr 
 |-  ( ( ph /\ { i , j } C_ B ) -> S C_ B )
45 44 sselda 
 |-  ( ( ( ph /\ { i , j } C_ B ) /\ k e. S ) -> k e. B )
46 6 3ad2ant1 
 |-  ( ( ph /\ i e. B /\ k e. B ) -> G e. Grp )
47 simp2 
 |-  ( ( ph /\ i e. B /\ k e. B ) -> i e. B )
48 1 10 25 9 grplinv 
 |-  ( ( G e. Grp /\ i e. B ) -> ( ( ( invg ` G ) ` i ) ( +g ` G ) i ) = ( 0g ` G ) )
49 46 47 48 syl2anc 
 |-  ( ( ph /\ i e. B /\ k e. B ) -> ( ( ( invg ` G ) ` i ) ( +g ` G ) i ) = ( 0g ` G ) )
50 49 oveq1d 
 |-  ( ( ph /\ i e. B /\ k e. B ) -> ( ( ( ( invg ` G ) ` i ) ( +g ` G ) i ) ( +g ` G ) k ) = ( ( 0g ` G ) ( +g ` G ) k ) )
51 46 47 29 syl2anc 
 |-  ( ( ph /\ i e. B /\ k e. B ) -> ( ( invg ` G ) ` i ) e. B )
52 simp3 
 |-  ( ( ph /\ i e. B /\ k e. B ) -> k e. B )
53 1 10 grpass 
 |-  ( ( G e. Grp /\ ( ( ( invg ` G ) ` i ) e. B /\ i e. B /\ k e. B ) ) -> ( ( ( ( invg ` G ) ` i ) ( +g ` G ) i ) ( +g ` G ) k ) = ( ( ( invg ` G ) ` i ) ( +g ` G ) ( i ( +g ` G ) k ) ) )
54 46 51 47 52 53 syl13anc 
 |-  ( ( ph /\ i e. B /\ k e. B ) -> ( ( ( ( invg ` G ) ` i ) ( +g ` G ) i ) ( +g ` G ) k ) = ( ( ( invg ` G ) ` i ) ( +g ` G ) ( i ( +g ` G ) k ) ) )
55 1 10 25 grplid 
 |-  ( ( G e. Grp /\ k e. B ) -> ( ( 0g ` G ) ( +g ` G ) k ) = k )
56 46 52 55 syl2anc 
 |-  ( ( ph /\ i e. B /\ k e. B ) -> ( ( 0g ` G ) ( +g ` G ) k ) = k )
57 50 54 56 3eqtr3d 
 |-  ( ( ph /\ i e. B /\ k e. B ) -> ( ( ( invg ` G ) ` i ) ( +g ` G ) ( i ( +g ` G ) k ) ) = k )
58 42 43 45 57 syl3anc 
 |-  ( ( ( ph /\ { i , j } C_ B ) /\ k e. S ) -> ( ( ( invg ` G ) ` i ) ( +g ` G ) ( i ( +g ` G ) k ) ) = k )
59 58 adantr 
 |-  ( ( ( ( ph /\ { i , j } C_ B ) /\ k e. S ) /\ ( i ( +g ` G ) k ) = j ) -> ( ( ( invg ` G ) ` i ) ( +g ` G ) ( i ( +g ` G ) k ) ) = k )
60 41 59 eqtr3d 
 |-  ( ( ( ( ph /\ { i , j } C_ B ) /\ k e. S ) /\ ( i ( +g ` G ) k ) = j ) -> ( ( ( invg ` G ) ` i ) ( +g ` G ) j ) = k )
61 simplr 
 |-  ( ( ( ( ph /\ { i , j } C_ B ) /\ k e. S ) /\ ( i ( +g ` G ) k ) = j ) -> k e. S )
62 60 61 eqeltrd 
 |-  ( ( ( ( ph /\ { i , j } C_ B ) /\ k e. S ) /\ ( i ( +g ` G ) k ) = j ) -> ( ( ( invg ` G ) ` i ) ( +g ` G ) j ) e. S )
63 62 r19.29an 
 |-  ( ( ( ph /\ { i , j } C_ B ) /\ E. k e. S ( i ( +g ` G ) k ) = j ) -> ( ( ( invg ` G ) ` i ) ( +g ` G ) j ) e. S )
64 39 63 impbida 
 |-  ( ( ph /\ { i , j } C_ B ) -> ( ( ( ( invg ` G ) ` i ) ( +g ` G ) j ) e. S <-> E. k e. S ( i ( +g ` G ) k ) = j ) )
65 64 pm5.32da 
 |-  ( ph -> ( ( { i , j } C_ B /\ ( ( ( invg ` G ) ` i ) ( +g ` G ) j ) e. S ) <-> ( { i , j } C_ B /\ E. k e. S ( i ( +g ` G ) k ) = j ) ) )
66 65 opabbidv 
 |-  ( ph -> { <. i , j >. | ( { i , j } C_ B /\ ( ( ( invg ` G ) ` i ) ( +g ` G ) j ) e. S ) } = { <. i , j >. | ( { i , j } C_ B /\ E. k e. S ( i ( +g ` G ) k ) = j ) } )
67 13 66 eqtrd 
 |-  ( ph -> ( G ~QG S ) = { <. i , j >. | ( { i , j } C_ B /\ E. k e. S ( i ( +g ` G ) k ) = j ) } )
68 67 eceq2d 
 |-  ( ph -> [ X ] ( G ~QG S ) = [ X ] { <. i , j >. | ( { i , j } C_ B /\ E. k e. S ( i ( +g ` G ) k ) = j ) } )
69 eqid 
 |-  { <. i , j >. | ( { i , j } C_ B /\ E. k e. S ( i ( +g ` G ) k ) = j ) } = { <. i , j >. | ( { i , j } C_ B /\ E. k e. S ( i ( +g ` G ) k ) = j ) }
70 6 grpmndd 
 |-  ( ph -> G e. Mnd )
71 1 10 2 69 70 8 4 lsmsnorb2 
 |-  ( ph -> ( { X } .(+) S ) = [ X ] { <. i , j >. | ( { i , j } C_ B /\ E. k e. S ( i ( +g ` G ) k ) = j ) } )
72 68 71 eqtr4d 
 |-  ( ph -> [ X ] ( G ~QG S ) = ( { X } .(+) S ) )