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

Metamath Proof Explorer

Theorem subglsm

Description: The subgroup sum evaluated within a subgroup. (Contributed by Mario Carneiro, 27-Apr-2016)

Ref Expression
Hypotheses subglsm.h ⊢ 𝐻 = ( 𝐺 ↾s 𝑆 )
subglsm.s ⊢ ⊕ = ( LSSum ‘ 𝐺 )
subglsm.a ⊢ 𝐴 = ( LSSum ‘ 𝐻 )
Assertion subglsm ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑇 ⊆ 𝑆 ∧ 𝑈 ⊆ 𝑆 ) → ( 𝑇 ⊕ 𝑈 ) = ( 𝑇 𝐴 𝑈 ) )

Proof

Step Hyp Ref Expression
1 subglsm.h ⊢ 𝐻 = ( 𝐺 ↾s 𝑆 )
2 subglsm.s ⊢ ⊕ = ( LSSum ‘ 𝐺 )
3 subglsm.a ⊢ 𝐴 = ( LSSum ‘ 𝐻 )
4 simp11 ⊢ ( ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑇 ⊆ 𝑆 ∧ 𝑈 ⊆ 𝑆 ) ∧ 𝑥 ∈ 𝑇 ∧ 𝑦 ∈ 𝑈 ) → 𝑆 ∈ ( SubGrp ‘ 𝐺 ) )
5 eqid ⊢ ( +g ‘ 𝐺 ) = ( +g ‘ 𝐺 )
6 1 5 ressplusg ⊢ ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) → ( +g ‘ 𝐺 ) = ( +g ‘ 𝐻 ) )
7 4 6 syl ⊢ ( ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑇 ⊆ 𝑆 ∧ 𝑈 ⊆ 𝑆 ) ∧ 𝑥 ∈ 𝑇 ∧ 𝑦 ∈ 𝑈 ) → ( +g ‘ 𝐺 ) = ( +g ‘ 𝐻 ) )
8 7 oveqd ⊢ ( ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑇 ⊆ 𝑆 ∧ 𝑈 ⊆ 𝑆 ) ∧ 𝑥 ∈ 𝑇 ∧ 𝑦 ∈ 𝑈 ) → ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) = ( 𝑥 ( +g ‘ 𝐻 ) 𝑦 ) )
9 8 mpoeq3dva ⊢ ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑇 ⊆ 𝑆 ∧ 𝑈 ⊆ 𝑆 ) → ( 𝑥 ∈ 𝑇 , 𝑦 ∈ 𝑈 ↦ ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ) = ( 𝑥 ∈ 𝑇 , 𝑦 ∈ 𝑈 ↦ ( 𝑥 ( +g ‘ 𝐻 ) 𝑦 ) ) )
10 9 rneqd ⊢ ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑇 ⊆ 𝑆 ∧ 𝑈 ⊆ 𝑆 ) → ran ( 𝑥 ∈ 𝑇 , 𝑦 ∈ 𝑈 ↦ ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ) = ran ( 𝑥 ∈ 𝑇 , 𝑦 ∈ 𝑈 ↦ ( 𝑥 ( +g ‘ 𝐻 ) 𝑦 ) ) )
11 subgrcl ⊢ ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) → 𝐺 ∈ Grp )
12 11 3ad2ant1 ⊢ ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑇 ⊆ 𝑆 ∧ 𝑈 ⊆ 𝑆 ) → 𝐺 ∈ Grp )
13 simp2 ⊢ ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑇 ⊆ 𝑆 ∧ 𝑈 ⊆ 𝑆 ) → 𝑇 ⊆ 𝑆 )
14 eqid ⊢ ( Base ‘ 𝐺 ) = ( Base ‘ 𝐺 )
15 14 subgss ⊢ ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) → 𝑆 ⊆ ( Base ‘ 𝐺 ) )
16 15 3ad2ant1 ⊢ ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑇 ⊆ 𝑆 ∧ 𝑈 ⊆ 𝑆 ) → 𝑆 ⊆ ( Base ‘ 𝐺 ) )
17 13 16 sstrd ⊢ ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑇 ⊆ 𝑆 ∧ 𝑈 ⊆ 𝑆 ) → 𝑇 ⊆ ( Base ‘ 𝐺 ) )
18 simp3 ⊢ ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑇 ⊆ 𝑆 ∧ 𝑈 ⊆ 𝑆 ) → 𝑈 ⊆ 𝑆 )
19 18 16 sstrd ⊢ ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑇 ⊆ 𝑆 ∧ 𝑈 ⊆ 𝑆 ) → 𝑈 ⊆ ( Base ‘ 𝐺 ) )
20 14 5 2 lsmvalx ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑇 ⊆ ( Base ‘ 𝐺 ) ∧ 𝑈 ⊆ ( Base ‘ 𝐺 ) ) → ( 𝑇 ⊕ 𝑈 ) = ran ( 𝑥 ∈ 𝑇 , 𝑦 ∈ 𝑈 ↦ ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ) )
21 12 17 19 20 syl3anc ⊢ ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑇 ⊆ 𝑆 ∧ 𝑈 ⊆ 𝑆 ) → ( 𝑇 ⊕ 𝑈 ) = ran ( 𝑥 ∈ 𝑇 , 𝑦 ∈ 𝑈 ↦ ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ) )
22 1 subggrp ⊢ ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) → 𝐻 ∈ Grp )
23 22 3ad2ant1 ⊢ ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑇 ⊆ 𝑆 ∧ 𝑈 ⊆ 𝑆 ) → 𝐻 ∈ Grp )
24 1 subgbas ⊢ ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) → 𝑆 = ( Base ‘ 𝐻 ) )
25 24 3ad2ant1 ⊢ ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑇 ⊆ 𝑆 ∧ 𝑈 ⊆ 𝑆 ) → 𝑆 = ( Base ‘ 𝐻 ) )
26 13 25 sseqtrd ⊢ ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑇 ⊆ 𝑆 ∧ 𝑈 ⊆ 𝑆 ) → 𝑇 ⊆ ( Base ‘ 𝐻 ) )
27 18 25 sseqtrd ⊢ ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑇 ⊆ 𝑆 ∧ 𝑈 ⊆ 𝑆 ) → 𝑈 ⊆ ( Base ‘ 𝐻 ) )
28 eqid ⊢ ( Base ‘ 𝐻 ) = ( Base ‘ 𝐻 )
29 eqid ⊢ ( +g ‘ 𝐻 ) = ( +g ‘ 𝐻 )
30 28 29 3 lsmvalx ⊢ ( ( 𝐻 ∈ Grp ∧ 𝑇 ⊆ ( Base ‘ 𝐻 ) ∧ 𝑈 ⊆ ( Base ‘ 𝐻 ) ) → ( 𝑇 𝐴 𝑈 ) = ran ( 𝑥 ∈ 𝑇 , 𝑦 ∈ 𝑈 ↦ ( 𝑥 ( +g ‘ 𝐻 ) 𝑦 ) ) )
31 23 26 27 30 syl3anc ⊢ ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑇 ⊆ 𝑆 ∧ 𝑈 ⊆ 𝑆 ) → ( 𝑇 𝐴 𝑈 ) = ran ( 𝑥 ∈ 𝑇 , 𝑦 ∈ 𝑈 ↦ ( 𝑥 ( +g ‘ 𝐻 ) 𝑦 ) ) )
32 10 21 31 3eqtr4d ⊢ ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑇 ⊆ 𝑆 ∧ 𝑈 ⊆ 𝑆 ) → ( 𝑇 ⊕ 𝑈 ) = ( 𝑇 𝐴 𝑈 ) )