Metamath Proof Explorer


Theorem lsmelvalm

Description: Subgroup sum membership analogue of lsmelval using vector subtraction. TODO: any way to shorten proof? (Contributed by NM, 16-Mar-2015) (Revised by Mario Carneiro, 19-Apr-2016)

Ref Expression
Hypotheses lsmelvalm.m = ( -g𝐺 )
lsmelvalm.p = ( LSSum ‘ 𝐺 )
lsmelvalm.t ( 𝜑𝑇 ∈ ( SubGrp ‘ 𝐺 ) )
lsmelvalm.u ( 𝜑𝑈 ∈ ( SubGrp ‘ 𝐺 ) )
Assertion lsmelvalm ( 𝜑 → ( 𝑋 ∈ ( 𝑇 𝑈 ) ↔ ∃ 𝑦𝑇𝑧𝑈 𝑋 = ( 𝑦 𝑧 ) ) )

Proof

Step Hyp Ref Expression
1 lsmelvalm.m = ( -g𝐺 )
2 lsmelvalm.p = ( LSSum ‘ 𝐺 )
3 lsmelvalm.t ( 𝜑𝑇 ∈ ( SubGrp ‘ 𝐺 ) )
4 lsmelvalm.u ( 𝜑𝑈 ∈ ( SubGrp ‘ 𝐺 ) )
5 eqid ( +g𝐺 ) = ( +g𝐺 )
6 5 2 lsmelval ( ( 𝑇 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑈 ∈ ( SubGrp ‘ 𝐺 ) ) → ( 𝑋 ∈ ( 𝑇 𝑈 ) ↔ ∃ 𝑦𝑇𝑥𝑈 𝑋 = ( 𝑦 ( +g𝐺 ) 𝑥 ) ) )
7 3 4 6 syl2anc ( 𝜑 → ( 𝑋 ∈ ( 𝑇 𝑈 ) ↔ ∃ 𝑦𝑇𝑥𝑈 𝑋 = ( 𝑦 ( +g𝐺 ) 𝑥 ) ) )
8 4 adantr ( ( 𝜑𝑦𝑇 ) → 𝑈 ∈ ( SubGrp ‘ 𝐺 ) )
9 eqid ( invg𝐺 ) = ( invg𝐺 )
10 9 subginvcl ( ( 𝑈 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑥𝑈 ) → ( ( invg𝐺 ) ‘ 𝑥 ) ∈ 𝑈 )
11 8 10 sylan ( ( ( 𝜑𝑦𝑇 ) ∧ 𝑥𝑈 ) → ( ( invg𝐺 ) ‘ 𝑥 ) ∈ 𝑈 )
12 eqid ( Base ‘ 𝐺 ) = ( Base ‘ 𝐺 )
13 subgrcl ( 𝑇 ∈ ( SubGrp ‘ 𝐺 ) → 𝐺 ∈ Grp )
14 3 13 syl ( 𝜑𝐺 ∈ Grp )
15 14 ad2antrr ( ( ( 𝜑𝑦𝑇 ) ∧ 𝑥𝑈 ) → 𝐺 ∈ Grp )
16 12 subgss ( 𝑇 ∈ ( SubGrp ‘ 𝐺 ) → 𝑇 ⊆ ( Base ‘ 𝐺 ) )
17 3 16 syl ( 𝜑𝑇 ⊆ ( Base ‘ 𝐺 ) )
18 17 sselda ( ( 𝜑𝑦𝑇 ) → 𝑦 ∈ ( Base ‘ 𝐺 ) )
19 18 adantr ( ( ( 𝜑𝑦𝑇 ) ∧ 𝑥𝑈 ) → 𝑦 ∈ ( Base ‘ 𝐺 ) )
20 12 subgss ( 𝑈 ∈ ( SubGrp ‘ 𝐺 ) → 𝑈 ⊆ ( Base ‘ 𝐺 ) )
21 8 20 syl ( ( 𝜑𝑦𝑇 ) → 𝑈 ⊆ ( Base ‘ 𝐺 ) )
22 21 sselda ( ( ( 𝜑𝑦𝑇 ) ∧ 𝑥𝑈 ) → 𝑥 ∈ ( Base ‘ 𝐺 ) )
23 12 5 1 9 15 19 22 grpsubinv ( ( ( 𝜑𝑦𝑇 ) ∧ 𝑥𝑈 ) → ( 𝑦 ( ( invg𝐺 ) ‘ 𝑥 ) ) = ( 𝑦 ( +g𝐺 ) 𝑥 ) )
24 23 eqcomd ( ( ( 𝜑𝑦𝑇 ) ∧ 𝑥𝑈 ) → ( 𝑦 ( +g𝐺 ) 𝑥 ) = ( 𝑦 ( ( invg𝐺 ) ‘ 𝑥 ) ) )
25 oveq2 ( 𝑧 = ( ( invg𝐺 ) ‘ 𝑥 ) → ( 𝑦 𝑧 ) = ( 𝑦 ( ( invg𝐺 ) ‘ 𝑥 ) ) )
26 25 rspceeqv ( ( ( ( invg𝐺 ) ‘ 𝑥 ) ∈ 𝑈 ∧ ( 𝑦 ( +g𝐺 ) 𝑥 ) = ( 𝑦 ( ( invg𝐺 ) ‘ 𝑥 ) ) ) → ∃ 𝑧𝑈 ( 𝑦 ( +g𝐺 ) 𝑥 ) = ( 𝑦 𝑧 ) )
27 11 24 26 syl2anc ( ( ( 𝜑𝑦𝑇 ) ∧ 𝑥𝑈 ) → ∃ 𝑧𝑈 ( 𝑦 ( +g𝐺 ) 𝑥 ) = ( 𝑦 𝑧 ) )
28 eqeq1 ( 𝑋 = ( 𝑦 ( +g𝐺 ) 𝑥 ) → ( 𝑋 = ( 𝑦 𝑧 ) ↔ ( 𝑦 ( +g𝐺 ) 𝑥 ) = ( 𝑦 𝑧 ) ) )
29 28 rexbidv ( 𝑋 = ( 𝑦 ( +g𝐺 ) 𝑥 ) → ( ∃ 𝑧𝑈 𝑋 = ( 𝑦 𝑧 ) ↔ ∃ 𝑧𝑈 ( 𝑦 ( +g𝐺 ) 𝑥 ) = ( 𝑦 𝑧 ) ) )
30 27 29 syl5ibrcom ( ( ( 𝜑𝑦𝑇 ) ∧ 𝑥𝑈 ) → ( 𝑋 = ( 𝑦 ( +g𝐺 ) 𝑥 ) → ∃ 𝑧𝑈 𝑋 = ( 𝑦 𝑧 ) ) )
31 30 rexlimdva ( ( 𝜑𝑦𝑇 ) → ( ∃ 𝑥𝑈 𝑋 = ( 𝑦 ( +g𝐺 ) 𝑥 ) → ∃ 𝑧𝑈 𝑋 = ( 𝑦 𝑧 ) ) )
32 9 subginvcl ( ( 𝑈 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑧𝑈 ) → ( ( invg𝐺 ) ‘ 𝑧 ) ∈ 𝑈 )
33 8 32 sylan ( ( ( 𝜑𝑦𝑇 ) ∧ 𝑧𝑈 ) → ( ( invg𝐺 ) ‘ 𝑧 ) ∈ 𝑈 )
34 18 adantr ( ( ( 𝜑𝑦𝑇 ) ∧ 𝑧𝑈 ) → 𝑦 ∈ ( Base ‘ 𝐺 ) )
35 21 sselda ( ( ( 𝜑𝑦𝑇 ) ∧ 𝑧𝑈 ) → 𝑧 ∈ ( Base ‘ 𝐺 ) )
36 12 5 9 1 grpsubval ( ( 𝑦 ∈ ( Base ‘ 𝐺 ) ∧ 𝑧 ∈ ( Base ‘ 𝐺 ) ) → ( 𝑦 𝑧 ) = ( 𝑦 ( +g𝐺 ) ( ( invg𝐺 ) ‘ 𝑧 ) ) )
37 34 35 36 syl2anc ( ( ( 𝜑𝑦𝑇 ) ∧ 𝑧𝑈 ) → ( 𝑦 𝑧 ) = ( 𝑦 ( +g𝐺 ) ( ( invg𝐺 ) ‘ 𝑧 ) ) )
38 oveq2 ( 𝑥 = ( ( invg𝐺 ) ‘ 𝑧 ) → ( 𝑦 ( +g𝐺 ) 𝑥 ) = ( 𝑦 ( +g𝐺 ) ( ( invg𝐺 ) ‘ 𝑧 ) ) )
39 38 rspceeqv ( ( ( ( invg𝐺 ) ‘ 𝑧 ) ∈ 𝑈 ∧ ( 𝑦 𝑧 ) = ( 𝑦 ( +g𝐺 ) ( ( invg𝐺 ) ‘ 𝑧 ) ) ) → ∃ 𝑥𝑈 ( 𝑦 𝑧 ) = ( 𝑦 ( +g𝐺 ) 𝑥 ) )
40 33 37 39 syl2anc ( ( ( 𝜑𝑦𝑇 ) ∧ 𝑧𝑈 ) → ∃ 𝑥𝑈 ( 𝑦 𝑧 ) = ( 𝑦 ( +g𝐺 ) 𝑥 ) )
41 eqeq1 ( 𝑋 = ( 𝑦 𝑧 ) → ( 𝑋 = ( 𝑦 ( +g𝐺 ) 𝑥 ) ↔ ( 𝑦 𝑧 ) = ( 𝑦 ( +g𝐺 ) 𝑥 ) ) )
42 41 rexbidv ( 𝑋 = ( 𝑦 𝑧 ) → ( ∃ 𝑥𝑈 𝑋 = ( 𝑦 ( +g𝐺 ) 𝑥 ) ↔ ∃ 𝑥𝑈 ( 𝑦 𝑧 ) = ( 𝑦 ( +g𝐺 ) 𝑥 ) ) )
43 40 42 syl5ibrcom ( ( ( 𝜑𝑦𝑇 ) ∧ 𝑧𝑈 ) → ( 𝑋 = ( 𝑦 𝑧 ) → ∃ 𝑥𝑈 𝑋 = ( 𝑦 ( +g𝐺 ) 𝑥 ) ) )
44 43 rexlimdva ( ( 𝜑𝑦𝑇 ) → ( ∃ 𝑧𝑈 𝑋 = ( 𝑦 𝑧 ) → ∃ 𝑥𝑈 𝑋 = ( 𝑦 ( +g𝐺 ) 𝑥 ) ) )
45 31 44 impbid ( ( 𝜑𝑦𝑇 ) → ( ∃ 𝑥𝑈 𝑋 = ( 𝑦 ( +g𝐺 ) 𝑥 ) ↔ ∃ 𝑧𝑈 𝑋 = ( 𝑦 𝑧 ) ) )
46 45 rexbidva ( 𝜑 → ( ∃ 𝑦𝑇𝑥𝑈 𝑋 = ( 𝑦 ( +g𝐺 ) 𝑥 ) ↔ ∃ 𝑦𝑇𝑧𝑈 𝑋 = ( 𝑦 𝑧 ) ) )
47 7 46 bitrd ( 𝜑 → ( 𝑋 ∈ ( 𝑇 𝑈 ) ↔ ∃ 𝑦𝑇𝑧𝑈 𝑋 = ( 𝑦 𝑧 ) ) )