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 ⊢ ( 𝜑 → ( 𝑋 ∈ ( 𝑇 ⊕ 𝑈 ) ↔ ∃ 𝑦 ∈ 𝑇 ∃ 𝑧 ∈ 𝑈 𝑋 = ( 𝑦 − 𝑧 ) ) )