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 ⊢ 𝐵 = ( Base ‘ 𝐺 )
quslsm.p ⊢ ⊕ = ( LSSum ‘ 𝐺 )
quslsm.n ⊢ ( 𝜑 → 𝑆 ∈ ( SubGrp ‘ 𝐺 ) )
quslsm.s ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
Assertion quslsm ( 𝜑 → [ 𝑋 ] ( 𝐺 ~QG 𝑆 ) = ( { 𝑋 } ⊕ 𝑆 ) )

Proof

Step Hyp Ref Expression
1 quslsm.b ⊢ 𝐵 = ( Base ‘ 𝐺 )
2 quslsm.p ⊢ ⊕ = ( LSSum ‘ 𝐺 )
3 quslsm.n ⊢ ( 𝜑 → 𝑆 ∈ ( SubGrp ‘ 𝐺 ) )
4 quslsm.s ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
5 subgrcl ⊢ ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) → 𝐺 ∈ Grp )
6 3 5 syl ⊢ ( 𝜑 → 𝐺 ∈ Grp )
7 1 subgss ⊢ ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) → 𝑆 ⊆ 𝐵 )
8 3 7 syl ⊢ ( 𝜑 → 𝑆 ⊆ 𝐵 )
9 eqid ⊢ ( invg ‘ 𝐺 ) = ( invg ‘ 𝐺 )
10 eqid ⊢ ( +g ‘ 𝐺 ) = ( +g ‘ 𝐺 )
11 eqid ⊢ ( 𝐺 ~QG 𝑆 ) = ( 𝐺 ~QG 𝑆 )
12 1 9 10 11 eqgfval ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑆 ⊆ 𝐵 ) → ( 𝐺 ~QG 𝑆 ) = { ⟨ 𝑖 , 𝑗 ⟩ ∣ ( { 𝑖 , 𝑗 } ⊆ 𝐵 ∧ ( ( ( invg ‘ 𝐺 ) ‘ 𝑖 ) ( +g ‘ 𝐺 ) 𝑗 ) ∈ 𝑆 ) } )
13 6 8 12 syl2anc ⊢ ( 𝜑 → ( 𝐺 ~QG 𝑆 ) = { ⟨ 𝑖 , 𝑗 ⟩ ∣ ( { 𝑖 , 𝑗 } ⊆ 𝐵 ∧ ( ( ( invg ‘ 𝐺 ) ‘ 𝑖 ) ( +g ‘ 𝐺 ) 𝑗 ) ∈ 𝑆 ) } )
14 simpr ⊢ ( ( ( 𝜑 ∧ { 𝑖 , 𝑗 } ⊆ 𝐵 ) ∧ ( ( ( invg ‘ 𝐺 ) ‘ 𝑖 ) ( +g ‘ 𝐺 ) 𝑗 ) ∈ 𝑆 ) → ( ( ( invg ‘ 𝐺 ) ‘ 𝑖 ) ( +g ‘ 𝐺 ) 𝑗 ) ∈ 𝑆 )
15 oveq2 ⊢ ( 𝑘 = ( ( ( invg ‘ 𝐺 ) ‘ 𝑖 ) ( +g ‘ 𝐺 ) 𝑗 ) → ( 𝑖 ( +g ‘ 𝐺 ) 𝑘 ) = ( 𝑖 ( +g ‘ 𝐺 ) ( ( ( invg ‘ 𝐺 ) ‘ 𝑖 ) ( +g ‘ 𝐺 ) 𝑗 ) ) )
16 15 eqeq1d ⊢ ( 𝑘 = ( ( ( invg ‘ 𝐺 ) ‘ 𝑖 ) ( +g ‘ 𝐺 ) 𝑗 ) → ( ( 𝑖 ( +g ‘ 𝐺 ) 𝑘 ) = 𝑗 ↔ ( 𝑖 ( +g ‘ 𝐺 ) ( ( ( invg ‘ 𝐺 ) ‘ 𝑖 ) ( +g ‘ 𝐺 ) 𝑗 ) ) = 𝑗 ) )
17 16 adantl ⊢ ( ( ( ( 𝜑 ∧ { 𝑖 , 𝑗 } ⊆ 𝐵 ) ∧ ( ( ( invg ‘ 𝐺 ) ‘ 𝑖 ) ( +g ‘ 𝐺 ) 𝑗 ) ∈ 𝑆 ) ∧ 𝑘 = ( ( ( invg ‘ 𝐺 ) ‘ 𝑖 ) ( +g ‘ 𝐺 ) 𝑗 ) ) → ( ( 𝑖 ( +g ‘ 𝐺 ) 𝑘 ) = 𝑗 ↔ ( 𝑖 ( +g ‘ 𝐺 ) ( ( ( invg ‘ 𝐺 ) ‘ 𝑖 ) ( +g ‘ 𝐺 ) 𝑗 ) ) = 𝑗 ) )
18 6 adantr ⊢ ( ( 𝜑 ∧ { 𝑖 , 𝑗 } ⊆ 𝐵 ) → 𝐺 ∈ Grp )
19 vex ⊢ 𝑖 ∈ V
20 vex ⊢ 𝑗 ∈ V
21 19 20 prss ⊢ ( ( 𝑖 ∈ 𝐵 ∧ 𝑗 ∈ 𝐵 ) ↔ { 𝑖 , 𝑗 } ⊆ 𝐵 )
22 21 bicomi ⊢ ( { 𝑖 , 𝑗 } ⊆ 𝐵 ↔ ( 𝑖 ∈ 𝐵 ∧ 𝑗 ∈ 𝐵 ) )
23 22 simplbi ⊢ ( { 𝑖 , 𝑗 } ⊆ 𝐵 → 𝑖 ∈ 𝐵 )
24 23 adantl ⊢ ( ( 𝜑 ∧ { 𝑖 , 𝑗 } ⊆ 𝐵 ) → 𝑖 ∈ 𝐵 )
25 eqid ⊢ ( 0g ‘ 𝐺 ) = ( 0g ‘ 𝐺 )
26 1 10 25 9 grprinv ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑖 ∈ 𝐵 ) → ( 𝑖 ( +g ‘ 𝐺 ) ( ( invg ‘ 𝐺 ) ‘ 𝑖 ) ) = ( 0g ‘ 𝐺 ) )
27 18 24 26 syl2anc ⊢ ( ( 𝜑 ∧ { 𝑖 , 𝑗 } ⊆ 𝐵 ) → ( 𝑖 ( +g ‘ 𝐺 ) ( ( invg ‘ 𝐺 ) ‘ 𝑖 ) ) = ( 0g ‘ 𝐺 ) )
28 27 oveq1d ⊢ ( ( 𝜑 ∧ { 𝑖 , 𝑗 } ⊆ 𝐵 ) → ( ( 𝑖 ( +g ‘ 𝐺 ) ( ( invg ‘ 𝐺 ) ‘ 𝑖 ) ) ( +g ‘ 𝐺 ) 𝑗 ) = ( ( 0g ‘ 𝐺 ) ( +g ‘ 𝐺 ) 𝑗 ) )
29 1 9 grpinvcl ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑖 ∈ 𝐵 ) → ( ( invg ‘ 𝐺 ) ‘ 𝑖 ) ∈ 𝐵 )
30 18 24 29 syl2anc ⊢ ( ( 𝜑 ∧ { 𝑖 , 𝑗 } ⊆ 𝐵 ) → ( ( invg ‘ 𝐺 ) ‘ 𝑖 ) ∈ 𝐵 )
31 22 simprbi ⊢ ( { 𝑖 , 𝑗 } ⊆ 𝐵 → 𝑗 ∈ 𝐵 )
32 31 adantl ⊢ ( ( 𝜑 ∧ { 𝑖 , 𝑗 } ⊆ 𝐵 ) → 𝑗 ∈ 𝐵 )
33 1 10 grpass ⊢ ( ( 𝐺 ∈ Grp ∧ ( 𝑖 ∈ 𝐵 ∧ ( ( invg ‘ 𝐺 ) ‘ 𝑖 ) ∈ 𝐵 ∧ 𝑗 ∈ 𝐵 ) ) → ( ( 𝑖 ( +g ‘ 𝐺 ) ( ( invg ‘ 𝐺 ) ‘ 𝑖 ) ) ( +g ‘ 𝐺 ) 𝑗 ) = ( 𝑖 ( +g ‘ 𝐺 ) ( ( ( invg ‘ 𝐺 ) ‘ 𝑖 ) ( +g ‘ 𝐺 ) 𝑗 ) ) )
34 18 24 30 32 33 syl13anc ⊢ ( ( 𝜑 ∧ { 𝑖 , 𝑗 } ⊆ 𝐵 ) → ( ( 𝑖 ( +g ‘ 𝐺 ) ( ( invg ‘ 𝐺 ) ‘ 𝑖 ) ) ( +g ‘ 𝐺 ) 𝑗 ) = ( 𝑖 ( +g ‘ 𝐺 ) ( ( ( invg ‘ 𝐺 ) ‘ 𝑖 ) ( +g ‘ 𝐺 ) 𝑗 ) ) )
35 1 10 25 grplid ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑗 ∈ 𝐵 ) → ( ( 0g ‘ 𝐺 ) ( +g ‘ 𝐺 ) 𝑗 ) = 𝑗 )
36 18 32 35 syl2anc ⊢ ( ( 𝜑 ∧ { 𝑖 , 𝑗 } ⊆ 𝐵 ) → ( ( 0g ‘ 𝐺 ) ( +g ‘ 𝐺 ) 𝑗 ) = 𝑗 )
37 28 34 36 3eqtr3d ⊢ ( ( 𝜑 ∧ { 𝑖 , 𝑗 } ⊆ 𝐵 ) → ( 𝑖 ( +g ‘ 𝐺 ) ( ( ( invg ‘ 𝐺 ) ‘ 𝑖 ) ( +g ‘ 𝐺 ) 𝑗 ) ) = 𝑗 )
38 37 adantr ⊢ ( ( ( 𝜑 ∧ { 𝑖 , 𝑗 } ⊆ 𝐵 ) ∧ ( ( ( invg ‘ 𝐺 ) ‘ 𝑖 ) ( +g ‘ 𝐺 ) 𝑗 ) ∈ 𝑆 ) → ( 𝑖 ( +g ‘ 𝐺 ) ( ( ( invg ‘ 𝐺 ) ‘ 𝑖 ) ( +g ‘ 𝐺 ) 𝑗 ) ) = 𝑗 )
39 14 17 38 rspcedvd ⊢ ( ( ( 𝜑 ∧ { 𝑖 , 𝑗 } ⊆ 𝐵 ) ∧ ( ( ( invg ‘ 𝐺 ) ‘ 𝑖 ) ( +g ‘ 𝐺 ) 𝑗 ) ∈ 𝑆 ) → ∃ 𝑘 ∈ 𝑆 ( 𝑖 ( +g ‘ 𝐺 ) 𝑘 ) = 𝑗 )
40 oveq2 ⊢ ( ( 𝑖 ( +g ‘ 𝐺 ) 𝑘 ) = 𝑗 → ( ( ( invg ‘ 𝐺 ) ‘ 𝑖 ) ( +g ‘ 𝐺 ) ( 𝑖 ( +g ‘ 𝐺 ) 𝑘 ) ) = ( ( ( invg ‘ 𝐺 ) ‘ 𝑖 ) ( +g ‘ 𝐺 ) 𝑗 ) )
41 40 adantl ⊢ ( ( ( ( 𝜑 ∧ { 𝑖 , 𝑗 } ⊆ 𝐵 ) ∧ 𝑘 ∈ 𝑆 ) ∧ ( 𝑖 ( +g ‘ 𝐺 ) 𝑘 ) = 𝑗 ) → ( ( ( invg ‘ 𝐺 ) ‘ 𝑖 ) ( +g ‘ 𝐺 ) ( 𝑖 ( +g ‘ 𝐺 ) 𝑘 ) ) = ( ( ( invg ‘ 𝐺 ) ‘ 𝑖 ) ( +g ‘ 𝐺 ) 𝑗 ) )
42 simpll ⊢ ( ( ( 𝜑 ∧ { 𝑖 , 𝑗 } ⊆ 𝐵 ) ∧ 𝑘 ∈ 𝑆 ) → 𝜑 )
43 24 adantr ⊢ ( ( ( 𝜑 ∧ { 𝑖 , 𝑗 } ⊆ 𝐵 ) ∧ 𝑘 ∈ 𝑆 ) → 𝑖 ∈ 𝐵 )
44 8 adantr ⊢ ( ( 𝜑 ∧ { 𝑖 , 𝑗 } ⊆ 𝐵 ) → 𝑆 ⊆ 𝐵 )
45 44 sselda ⊢ ( ( ( 𝜑 ∧ { 𝑖 , 𝑗 } ⊆ 𝐵 ) ∧ 𝑘 ∈ 𝑆 ) → 𝑘 ∈ 𝐵 )
46 6 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝐵 ∧ 𝑘 ∈ 𝐵 ) → 𝐺 ∈ Grp )
47 simp2 ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝐵 ∧ 𝑘 ∈ 𝐵 ) → 𝑖 ∈ 𝐵 )
48 1 10 25 9 grplinv ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑖 ∈ 𝐵 ) → ( ( ( invg ‘ 𝐺 ) ‘ 𝑖 ) ( +g ‘ 𝐺 ) 𝑖 ) = ( 0g ‘ 𝐺 ) )
49 46 47 48 syl2anc ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝐵 ∧ 𝑘 ∈ 𝐵 ) → ( ( ( invg ‘ 𝐺 ) ‘ 𝑖 ) ( +g ‘ 𝐺 ) 𝑖 ) = ( 0g ‘ 𝐺 ) )
50 49 oveq1d ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝐵 ∧ 𝑘 ∈ 𝐵 ) → ( ( ( ( invg ‘ 𝐺 ) ‘ 𝑖 ) ( +g ‘ 𝐺 ) 𝑖 ) ( +g ‘ 𝐺 ) 𝑘 ) = ( ( 0g ‘ 𝐺 ) ( +g ‘ 𝐺 ) 𝑘 ) )
51 46 47 29 syl2anc ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝐵 ∧ 𝑘 ∈ 𝐵 ) → ( ( invg ‘ 𝐺 ) ‘ 𝑖 ) ∈ 𝐵 )
52 simp3 ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝐵 ∧ 𝑘 ∈ 𝐵 ) → 𝑘 ∈ 𝐵 )
53 1 10 grpass ⊢ ( ( 𝐺 ∈ Grp ∧ ( ( ( invg ‘ 𝐺 ) ‘ 𝑖 ) ∈ 𝐵 ∧ 𝑖 ∈ 𝐵 ∧ 𝑘 ∈ 𝐵 ) ) → ( ( ( ( invg ‘ 𝐺 ) ‘ 𝑖 ) ( +g ‘ 𝐺 ) 𝑖 ) ( +g ‘ 𝐺 ) 𝑘 ) = ( ( ( invg ‘ 𝐺 ) ‘ 𝑖 ) ( +g ‘ 𝐺 ) ( 𝑖 ( +g ‘ 𝐺 ) 𝑘 ) ) )
54 46 51 47 52 53 syl13anc ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝐵 ∧ 𝑘 ∈ 𝐵 ) → ( ( ( ( invg ‘ 𝐺 ) ‘ 𝑖 ) ( +g ‘ 𝐺 ) 𝑖 ) ( +g ‘ 𝐺 ) 𝑘 ) = ( ( ( invg ‘ 𝐺 ) ‘ 𝑖 ) ( +g ‘ 𝐺 ) ( 𝑖 ( +g ‘ 𝐺 ) 𝑘 ) ) )
55 1 10 25 grplid ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑘 ∈ 𝐵 ) → ( ( 0g ‘ 𝐺 ) ( +g ‘ 𝐺 ) 𝑘 ) = 𝑘 )
56 46 52 55 syl2anc ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝐵 ∧ 𝑘 ∈ 𝐵 ) → ( ( 0g ‘ 𝐺 ) ( +g ‘ 𝐺 ) 𝑘 ) = 𝑘 )
57 50 54 56 3eqtr3d ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝐵 ∧ 𝑘 ∈ 𝐵 ) → ( ( ( invg ‘ 𝐺 ) ‘ 𝑖 ) ( +g ‘ 𝐺 ) ( 𝑖 ( +g ‘ 𝐺 ) 𝑘 ) ) = 𝑘 )
58 42 43 45 57 syl3anc ⊢ ( ( ( 𝜑 ∧ { 𝑖 , 𝑗 } ⊆ 𝐵 ) ∧ 𝑘 ∈ 𝑆 ) → ( ( ( invg ‘ 𝐺 ) ‘ 𝑖 ) ( +g ‘ 𝐺 ) ( 𝑖 ( +g ‘ 𝐺 ) 𝑘 ) ) = 𝑘 )
59 58 adantr ⊢ ( ( ( ( 𝜑 ∧ { 𝑖 , 𝑗 } ⊆ 𝐵 ) ∧ 𝑘 ∈ 𝑆 ) ∧ ( 𝑖 ( +g ‘ 𝐺 ) 𝑘 ) = 𝑗 ) → ( ( ( invg ‘ 𝐺 ) ‘ 𝑖 ) ( +g ‘ 𝐺 ) ( 𝑖 ( +g ‘ 𝐺 ) 𝑘 ) ) = 𝑘 )
60 41 59 eqtr3d ⊢ ( ( ( ( 𝜑 ∧ { 𝑖 , 𝑗 } ⊆ 𝐵 ) ∧ 𝑘 ∈ 𝑆 ) ∧ ( 𝑖 ( +g ‘ 𝐺 ) 𝑘 ) = 𝑗 ) → ( ( ( invg ‘ 𝐺 ) ‘ 𝑖 ) ( +g ‘ 𝐺 ) 𝑗 ) = 𝑘 )
61 simplr ⊢ ( ( ( ( 𝜑 ∧ { 𝑖 , 𝑗 } ⊆ 𝐵 ) ∧ 𝑘 ∈ 𝑆 ) ∧ ( 𝑖 ( +g ‘ 𝐺 ) 𝑘 ) = 𝑗 ) → 𝑘 ∈ 𝑆 )
62 60 61 eqeltrd ⊢ ( ( ( ( 𝜑 ∧ { 𝑖 , 𝑗 } ⊆ 𝐵 ) ∧ 𝑘 ∈ 𝑆 ) ∧ ( 𝑖 ( +g ‘ 𝐺 ) 𝑘 ) = 𝑗 ) → ( ( ( invg ‘ 𝐺 ) ‘ 𝑖 ) ( +g ‘ 𝐺 ) 𝑗 ) ∈ 𝑆 )
63 62 r19.29an ⊢ ( ( ( 𝜑 ∧ { 𝑖 , 𝑗 } ⊆ 𝐵 ) ∧ ∃ 𝑘 ∈ 𝑆 ( 𝑖 ( +g ‘ 𝐺 ) 𝑘 ) = 𝑗 ) → ( ( ( invg ‘ 𝐺 ) ‘ 𝑖 ) ( +g ‘ 𝐺 ) 𝑗 ) ∈ 𝑆 )
64 39 63 impbida ⊢ ( ( 𝜑 ∧ { 𝑖 , 𝑗 } ⊆ 𝐵 ) → ( ( ( ( invg ‘ 𝐺 ) ‘ 𝑖 ) ( +g ‘ 𝐺 ) 𝑗 ) ∈ 𝑆 ↔ ∃ 𝑘 ∈ 𝑆 ( 𝑖 ( +g ‘ 𝐺 ) 𝑘 ) = 𝑗 ) )
65 64 pm5.32da ⊢ ( 𝜑 → ( ( { 𝑖 , 𝑗 } ⊆ 𝐵 ∧ ( ( ( invg ‘ 𝐺 ) ‘ 𝑖 ) ( +g ‘ 𝐺 ) 𝑗 ) ∈ 𝑆 ) ↔ ( { 𝑖 , 𝑗 } ⊆ 𝐵 ∧ ∃ 𝑘 ∈ 𝑆 ( 𝑖 ( +g ‘ 𝐺 ) 𝑘 ) = 𝑗 ) ) )
66 65 opabbidv ⊢ ( 𝜑 → { ⟨ 𝑖 , 𝑗 ⟩ ∣ ( { 𝑖 , 𝑗 } ⊆ 𝐵 ∧ ( ( ( invg ‘ 𝐺 ) ‘ 𝑖 ) ( +g ‘ 𝐺 ) 𝑗 ) ∈ 𝑆 ) } = { ⟨ 𝑖 , 𝑗 ⟩ ∣ ( { 𝑖 , 𝑗 } ⊆ 𝐵 ∧ ∃ 𝑘 ∈ 𝑆 ( 𝑖 ( +g ‘ 𝐺 ) 𝑘 ) = 𝑗 ) } )
67 13 66 eqtrd ⊢ ( 𝜑 → ( 𝐺 ~QG 𝑆 ) = { ⟨ 𝑖 , 𝑗 ⟩ ∣ ( { 𝑖 , 𝑗 } ⊆ 𝐵 ∧ ∃ 𝑘 ∈ 𝑆 ( 𝑖 ( +g ‘ 𝐺 ) 𝑘 ) = 𝑗 ) } )
68 67 eceq2d ⊢ ( 𝜑 → [ 𝑋 ] ( 𝐺 ~QG 𝑆 ) = [ 𝑋 ] { ⟨ 𝑖 , 𝑗 ⟩ ∣ ( { 𝑖 , 𝑗 } ⊆ 𝐵 ∧ ∃ 𝑘 ∈ 𝑆 ( 𝑖 ( +g ‘ 𝐺 ) 𝑘 ) = 𝑗 ) } )
69 eqid ⊢ { ⟨ 𝑖 , 𝑗 ⟩ ∣ ( { 𝑖 , 𝑗 } ⊆ 𝐵 ∧ ∃ 𝑘 ∈ 𝑆 ( 𝑖 ( +g ‘ 𝐺 ) 𝑘 ) = 𝑗 ) } = { ⟨ 𝑖 , 𝑗 ⟩ ∣ ( { 𝑖 , 𝑗 } ⊆ 𝐵 ∧ ∃ 𝑘 ∈ 𝑆 ( 𝑖 ( +g ‘ 𝐺 ) 𝑘 ) = 𝑗 ) }
70 6 grpmndd ⊢ ( 𝜑 → 𝐺 ∈ Mnd )
71 1 10 2 69 70 8 4 lsmsnorb2 ⊢ ( 𝜑 → ( { 𝑋 } ⊕ 𝑆 ) = [ 𝑋 ] { ⟨ 𝑖 , 𝑗 ⟩ ∣ ( { 𝑖 , 𝑗 } ⊆ 𝐵 ∧ ∃ 𝑘 ∈ 𝑆 ( 𝑖 ( +g ‘ 𝐺 ) 𝑘 ) = 𝑗 ) } )
72 68 71 eqtr4d ⊢ ( 𝜑 → [ 𝑋 ] ( 𝐺 ~QG 𝑆 ) = ( { 𝑋 } ⊕ 𝑆 ) )