Metamath Proof Explorer

Theorem mapdpglem24

Description: Lemma for mapdpg . Existence part - consolidate hypotheses in mapdpglem23 . (Contributed by NM, 21-Mar-2015)

Ref Expression
Hypotheses mapdpg.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
mapdpg.m ⊢ 𝑀 = ( ( mapd ‘ 𝐾 ) ‘ 𝑊 )
mapdpg.u ⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
mapdpg.v ⊢ 𝑉 = ( Base ‘ 𝑈 )
mapdpg.s ⊢ − = ( -g ‘ 𝑈 )
mapdpg.z ⊢ 0 = ( 0g ‘ 𝑈 )
mapdpg.n ⊢ 𝑁 = ( LSpan ‘ 𝑈 )
mapdpg.c ⊢ 𝐶 = ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 )
mapdpg.f ⊢ 𝐹 = ( Base ‘ 𝐶 )
mapdpg.r ⊢ 𝑅 = ( -g ‘ 𝐶 )
mapdpg.j ⊢ 𝐽 = ( LSpan ‘ 𝐶 )
mapdpg.k ⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
mapdpg.x ⊢ ( 𝜑 → 𝑋 ∈ ( 𝑉 ∖ { 0 } ) )
mapdpg.y ⊢ ( 𝜑 → 𝑌 ∈ ( 𝑉 ∖ { 0 } ) )
mapdpg.g ⊢ ( 𝜑 → 𝐺 ∈ 𝐹 )
mapdpg.ne ⊢ ( 𝜑 → ( 𝑁 ‘ { 𝑋 } ) ≠ ( 𝑁 ‘ { 𝑌 } ) )
mapdpg.e ⊢ ( 𝜑 → ( 𝑀 ‘ ( 𝑁 ‘ { 𝑋 } ) ) = ( 𝐽 ‘ { 𝐺 } ) )
Assertion mapdpglem24 ( 𝜑 → ∃ ℎ ∈ 𝐹 ( ( 𝑀 ‘ ( 𝑁 ‘ { 𝑌 } ) ) = ( 𝐽 ‘ { ℎ } ) ∧ ( 𝑀 ‘ ( 𝑁 ‘ { ( 𝑋 − 𝑌 ) } ) ) = ( 𝐽 ‘ { ( 𝐺 𝑅 ℎ ) } ) ) )

Proof

Step Hyp Ref Expression
1 mapdpg.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
2 mapdpg.m ⊢ 𝑀 = ( ( mapd ‘ 𝐾 ) ‘ 𝑊 )
3 mapdpg.u ⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
4 mapdpg.v ⊢ 𝑉 = ( Base ‘ 𝑈 )
5 mapdpg.s ⊢ − = ( -g ‘ 𝑈 )
6 mapdpg.z ⊢ 0 = ( 0g ‘ 𝑈 )
7 mapdpg.n ⊢ 𝑁 = ( LSpan ‘ 𝑈 )
8 mapdpg.c ⊢ 𝐶 = ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 )
9 mapdpg.f ⊢ 𝐹 = ( Base ‘ 𝐶 )
10 mapdpg.r ⊢ 𝑅 = ( -g ‘ 𝐶 )
11 mapdpg.j ⊢ 𝐽 = ( LSpan ‘ 𝐶 )
12 mapdpg.k ⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
13 mapdpg.x ⊢ ( 𝜑 → 𝑋 ∈ ( 𝑉 ∖ { 0 } ) )
14 mapdpg.y ⊢ ( 𝜑 → 𝑌 ∈ ( 𝑉 ∖ { 0 } ) )
15 mapdpg.g ⊢ ( 𝜑 → 𝐺 ∈ 𝐹 )
16 mapdpg.ne ⊢ ( 𝜑 → ( 𝑁 ‘ { 𝑋 } ) ≠ ( 𝑁 ‘ { 𝑌 } ) )
17 mapdpg.e ⊢ ( 𝜑 → ( 𝑀 ‘ ( 𝑁 ‘ { 𝑋 } ) ) = ( 𝐽 ‘ { 𝐺 } ) )
18 13 eldifad ⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
19 14 eldifad ⊢ ( 𝜑 → 𝑌 ∈ 𝑉 )
20 eqid ⊢ ( LSSum ‘ 𝐶 ) = ( LSSum ‘ 𝐶 )
21 1 2 3 4 5 7 8 12 18 19 20 11 mapdpglem2 ⊢ ( 𝜑 → ∃ 𝑡 ∈ ( ( 𝑀 ‘ ( 𝑁 ‘ { 𝑋 } ) ) ( LSSum ‘ 𝐶 ) ( 𝑀 ‘ ( 𝑁 ‘ { 𝑌 } ) ) ) ( 𝑀 ‘ ( 𝑁 ‘ { ( 𝑋 − 𝑌 ) } ) ) = ( 𝐽 ‘ { 𝑡 } ) )
22 12 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( ( 𝑀 ‘ ( 𝑁 ‘ { 𝑋 } ) ) ( LSSum ‘ 𝐶 ) ( 𝑀 ‘ ( 𝑁 ‘ { 𝑌 } ) ) ) ∧ ( 𝑀 ‘ ( 𝑁 ‘ { ( 𝑋 − 𝑌 ) } ) ) = ( 𝐽 ‘ { 𝑡 } ) ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
23 18 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( ( 𝑀 ‘ ( 𝑁 ‘ { 𝑋 } ) ) ( LSSum ‘ 𝐶 ) ( 𝑀 ‘ ( 𝑁 ‘ { 𝑌 } ) ) ) ∧ ( 𝑀 ‘ ( 𝑁 ‘ { ( 𝑋 − 𝑌 ) } ) ) = ( 𝐽 ‘ { 𝑡 } ) ) → 𝑋 ∈ 𝑉 )
24 19 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( ( 𝑀 ‘ ( 𝑁 ‘ { 𝑋 } ) ) ( LSSum ‘ 𝐶 ) ( 𝑀 ‘ ( 𝑁 ‘ { 𝑌 } ) ) ) ∧ ( 𝑀 ‘ ( 𝑁 ‘ { ( 𝑋 − 𝑌 ) } ) ) = ( 𝐽 ‘ { 𝑡 } ) ) → 𝑌 ∈ 𝑉 )
25 simp2 ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( ( 𝑀 ‘ ( 𝑁 ‘ { 𝑋 } ) ) ( LSSum ‘ 𝐶 ) ( 𝑀 ‘ ( 𝑁 ‘ { 𝑌 } ) ) ) ∧ ( 𝑀 ‘ ( 𝑁 ‘ { ( 𝑋 − 𝑌 ) } ) ) = ( 𝐽 ‘ { 𝑡 } ) ) → 𝑡 ∈ ( ( 𝑀 ‘ ( 𝑁 ‘ { 𝑋 } ) ) ( LSSum ‘ 𝐶 ) ( 𝑀 ‘ ( 𝑁 ‘ { 𝑌 } ) ) ) )
26 eqid ⊢ ( Scalar ‘ 𝑈 ) = ( Scalar ‘ 𝑈 )
27 eqid ⊢ ( Base ‘ ( Scalar ‘ 𝑈 ) ) = ( Base ‘ ( Scalar ‘ 𝑈 ) )
28 eqid ⊢ ( ·𝑠 ‘ 𝐶 ) = ( ·𝑠 ‘ 𝐶 )
29 15 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( ( 𝑀 ‘ ( 𝑁 ‘ { 𝑋 } ) ) ( LSSum ‘ 𝐶 ) ( 𝑀 ‘ ( 𝑁 ‘ { 𝑌 } ) ) ) ∧ ( 𝑀 ‘ ( 𝑁 ‘ { ( 𝑋 − 𝑌 ) } ) ) = ( 𝐽 ‘ { 𝑡 } ) ) → 𝐺 ∈ 𝐹 )
30 17 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( ( 𝑀 ‘ ( 𝑁 ‘ { 𝑋 } ) ) ( LSSum ‘ 𝐶 ) ( 𝑀 ‘ ( 𝑁 ‘ { 𝑌 } ) ) ) ∧ ( 𝑀 ‘ ( 𝑁 ‘ { ( 𝑋 − 𝑌 ) } ) ) = ( 𝐽 ‘ { 𝑡 } ) ) → ( 𝑀 ‘ ( 𝑁 ‘ { 𝑋 } ) ) = ( 𝐽 ‘ { 𝐺 } ) )
31 1 2 3 4 5 7 8 22 23 24 20 11 9 25 26 27 28 10 29 30 mapdpglem3 ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( ( 𝑀 ‘ ( 𝑁 ‘ { 𝑋 } ) ) ( LSSum ‘ 𝐶 ) ( 𝑀 ‘ ( 𝑁 ‘ { 𝑌 } ) ) ) ∧ ( 𝑀 ‘ ( 𝑁 ‘ { ( 𝑋 − 𝑌 ) } ) ) = ( 𝐽 ‘ { 𝑡 } ) ) → ∃ 𝑔 ∈ ( Base ‘ ( Scalar ‘ 𝑈 ) ) ∃ 𝑧 ∈ ( 𝑀 ‘ ( 𝑁 ‘ { 𝑌 } ) ) 𝑡 = ( ( 𝑔 ( ·𝑠 ‘ 𝐶 ) 𝐺 ) 𝑅 𝑧 ) )
32 22 3ad2ant1 ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ ( ( 𝑀 ‘ ( 𝑁 ‘ { 𝑋 } ) ) ( LSSum ‘ 𝐶 ) ( 𝑀 ‘ ( 𝑁 ‘ { 𝑌 } ) ) ) ∧ ( 𝑀 ‘ ( 𝑁 ‘ { ( 𝑋 − 𝑌 ) } ) ) = ( 𝐽 ‘ { 𝑡 } ) ) ∧ ( 𝑔 ∈ ( Base ‘ ( Scalar ‘ 𝑈 ) ) ∧ 𝑧 ∈ ( 𝑀 ‘ ( 𝑁 ‘ { 𝑌 } ) ) ) ∧ 𝑡 = ( ( 𝑔 ( ·𝑠 ‘ 𝐶 ) 𝐺 ) 𝑅 𝑧 ) ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
33 23 3ad2ant1 ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ ( ( 𝑀 ‘ ( 𝑁 ‘ { 𝑋 } ) ) ( LSSum ‘ 𝐶 ) ( 𝑀 ‘ ( 𝑁 ‘ { 𝑌 } ) ) ) ∧ ( 𝑀 ‘ ( 𝑁 ‘ { ( 𝑋 − 𝑌 ) } ) ) = ( 𝐽 ‘ { 𝑡 } ) ) ∧ ( 𝑔 ∈ ( Base ‘ ( Scalar ‘ 𝑈 ) ) ∧ 𝑧 ∈ ( 𝑀 ‘ ( 𝑁 ‘ { 𝑌 } ) ) ) ∧ 𝑡 = ( ( 𝑔 ( ·𝑠 ‘ 𝐶 ) 𝐺 ) 𝑅 𝑧 ) ) → 𝑋 ∈ 𝑉 )
34 24 3ad2ant1 ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ ( ( 𝑀 ‘ ( 𝑁 ‘ { 𝑋 } ) ) ( LSSum ‘ 𝐶 ) ( 𝑀 ‘ ( 𝑁 ‘ { 𝑌 } ) ) ) ∧ ( 𝑀 ‘ ( 𝑁 ‘ { ( 𝑋 − 𝑌 ) } ) ) = ( 𝐽 ‘ { 𝑡 } ) ) ∧ ( 𝑔 ∈ ( Base ‘ ( Scalar ‘ 𝑈 ) ) ∧ 𝑧 ∈ ( 𝑀 ‘ ( 𝑁 ‘ { 𝑌 } ) ) ) ∧ 𝑡 = ( ( 𝑔 ( ·𝑠 ‘ 𝐶 ) 𝐺 ) 𝑅 𝑧 ) ) → 𝑌 ∈ 𝑉 )
35 simp12 ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ ( ( 𝑀 ‘ ( 𝑁 ‘ { 𝑋 } ) ) ( LSSum ‘ 𝐶 ) ( 𝑀 ‘ ( 𝑁 ‘ { 𝑌 } ) ) ) ∧ ( 𝑀 ‘ ( 𝑁 ‘ { ( 𝑋 − 𝑌 ) } ) ) = ( 𝐽 ‘ { 𝑡 } ) ) ∧ ( 𝑔 ∈ ( Base ‘ ( Scalar ‘ 𝑈 ) ) ∧ 𝑧 ∈ ( 𝑀 ‘ ( 𝑁 ‘ { 𝑌 } ) ) ) ∧ 𝑡 = ( ( 𝑔 ( ·𝑠 ‘ 𝐶 ) 𝐺 ) 𝑅 𝑧 ) ) → 𝑡 ∈ ( ( 𝑀 ‘ ( 𝑁 ‘ { 𝑋 } ) ) ( LSSum ‘ 𝐶 ) ( 𝑀 ‘ ( 𝑁 ‘ { 𝑌 } ) ) ) )
36 29 3ad2ant1 ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ ( ( 𝑀 ‘ ( 𝑁 ‘ { 𝑋 } ) ) ( LSSum ‘ 𝐶 ) ( 𝑀 ‘ ( 𝑁 ‘ { 𝑌 } ) ) ) ∧ ( 𝑀 ‘ ( 𝑁 ‘ { ( 𝑋 − 𝑌 ) } ) ) = ( 𝐽 ‘ { 𝑡 } ) ) ∧ ( 𝑔 ∈ ( Base ‘ ( Scalar ‘ 𝑈 ) ) ∧ 𝑧 ∈ ( 𝑀 ‘ ( 𝑁 ‘ { 𝑌 } ) ) ) ∧ 𝑡 = ( ( 𝑔 ( ·𝑠 ‘ 𝐶 ) 𝐺 ) 𝑅 𝑧 ) ) → 𝐺 ∈ 𝐹 )
37 30 3ad2ant1 ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ ( ( 𝑀 ‘ ( 𝑁 ‘ { 𝑋 } ) ) ( LSSum ‘ 𝐶 ) ( 𝑀 ‘ ( 𝑁 ‘ { 𝑌 } ) ) ) ∧ ( 𝑀 ‘ ( 𝑁 ‘ { ( 𝑋 − 𝑌 ) } ) ) = ( 𝐽 ‘ { 𝑡 } ) ) ∧ ( 𝑔 ∈ ( Base ‘ ( Scalar ‘ 𝑈 ) ) ∧ 𝑧 ∈ ( 𝑀 ‘ ( 𝑁 ‘ { 𝑌 } ) ) ) ∧ 𝑡 = ( ( 𝑔 ( ·𝑠 ‘ 𝐶 ) 𝐺 ) 𝑅 𝑧 ) ) → ( 𝑀 ‘ ( 𝑁 ‘ { 𝑋 } ) ) = ( 𝐽 ‘ { 𝐺 } ) )
38 16 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( ( 𝑀 ‘ ( 𝑁 ‘ { 𝑋 } ) ) ( LSSum ‘ 𝐶 ) ( 𝑀 ‘ ( 𝑁 ‘ { 𝑌 } ) ) ) ∧ ( 𝑀 ‘ ( 𝑁 ‘ { ( 𝑋 − 𝑌 ) } ) ) = ( 𝐽 ‘ { 𝑡 } ) ) → ( 𝑁 ‘ { 𝑋 } ) ≠ ( 𝑁 ‘ { 𝑌 } ) )
39 38 3ad2ant1 ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ ( ( 𝑀 ‘ ( 𝑁 ‘ { 𝑋 } ) ) ( LSSum ‘ 𝐶 ) ( 𝑀 ‘ ( 𝑁 ‘ { 𝑌 } ) ) ) ∧ ( 𝑀 ‘ ( 𝑁 ‘ { ( 𝑋 − 𝑌 ) } ) ) = ( 𝐽 ‘ { 𝑡 } ) ) ∧ ( 𝑔 ∈ ( Base ‘ ( Scalar ‘ 𝑈 ) ) ∧ 𝑧 ∈ ( 𝑀 ‘ ( 𝑁 ‘ { 𝑌 } ) ) ) ∧ 𝑡 = ( ( 𝑔 ( ·𝑠 ‘ 𝐶 ) 𝐺 ) 𝑅 𝑧 ) ) → ( 𝑁 ‘ { 𝑋 } ) ≠ ( 𝑁 ‘ { 𝑌 } ) )
40 simp13 ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ ( ( 𝑀 ‘ ( 𝑁 ‘ { 𝑋 } ) ) ( LSSum ‘ 𝐶 ) ( 𝑀 ‘ ( 𝑁 ‘ { 𝑌 } ) ) ) ∧ ( 𝑀 ‘ ( 𝑁 ‘ { ( 𝑋 − 𝑌 ) } ) ) = ( 𝐽 ‘ { 𝑡 } ) ) ∧ ( 𝑔 ∈ ( Base ‘ ( Scalar ‘ 𝑈 ) ) ∧ 𝑧 ∈ ( 𝑀 ‘ ( 𝑁 ‘ { 𝑌 } ) ) ) ∧ 𝑡 = ( ( 𝑔 ( ·𝑠 ‘ 𝐶 ) 𝐺 ) 𝑅 𝑧 ) ) → ( 𝑀 ‘ ( 𝑁 ‘ { ( 𝑋 − 𝑌 ) } ) ) = ( 𝐽 ‘ { 𝑡 } ) )
41 eqid ⊢ ( 0g ‘ ( Scalar ‘ 𝑈 ) ) = ( 0g ‘ ( Scalar ‘ 𝑈 ) )
42 simp2l ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ ( ( 𝑀 ‘ ( 𝑁 ‘ { 𝑋 } ) ) ( LSSum ‘ 𝐶 ) ( 𝑀 ‘ ( 𝑁 ‘ { 𝑌 } ) ) ) ∧ ( 𝑀 ‘ ( 𝑁 ‘ { ( 𝑋 − 𝑌 ) } ) ) = ( 𝐽 ‘ { 𝑡 } ) ) ∧ ( 𝑔 ∈ ( Base ‘ ( Scalar ‘ 𝑈 ) ) ∧ 𝑧 ∈ ( 𝑀 ‘ ( 𝑁 ‘ { 𝑌 } ) ) ) ∧ 𝑡 = ( ( 𝑔 ( ·𝑠 ‘ 𝐶 ) 𝐺 ) 𝑅 𝑧 ) ) → 𝑔 ∈ ( Base ‘ ( Scalar ‘ 𝑈 ) ) )
43 simp2r ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ ( ( 𝑀 ‘ ( 𝑁 ‘ { 𝑋 } ) ) ( LSSum ‘ 𝐶 ) ( 𝑀 ‘ ( 𝑁 ‘ { 𝑌 } ) ) ) ∧ ( 𝑀 ‘ ( 𝑁 ‘ { ( 𝑋 − 𝑌 ) } ) ) = ( 𝐽 ‘ { 𝑡 } ) ) ∧ ( 𝑔 ∈ ( Base ‘ ( Scalar ‘ 𝑈 ) ) ∧ 𝑧 ∈ ( 𝑀 ‘ ( 𝑁 ‘ { 𝑌 } ) ) ) ∧ 𝑡 = ( ( 𝑔 ( ·𝑠 ‘ 𝐶 ) 𝐺 ) 𝑅 𝑧 ) ) → 𝑧 ∈ ( 𝑀 ‘ ( 𝑁 ‘ { 𝑌 } ) ) )
44 simp3 ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ ( ( 𝑀 ‘ ( 𝑁 ‘ { 𝑋 } ) ) ( LSSum ‘ 𝐶 ) ( 𝑀 ‘ ( 𝑁 ‘ { 𝑌 } ) ) ) ∧ ( 𝑀 ‘ ( 𝑁 ‘ { ( 𝑋 − 𝑌 ) } ) ) = ( 𝐽 ‘ { 𝑡 } ) ) ∧ ( 𝑔 ∈ ( Base ‘ ( Scalar ‘ 𝑈 ) ) ∧ 𝑧 ∈ ( 𝑀 ‘ ( 𝑁 ‘ { 𝑌 } ) ) ) ∧ 𝑡 = ( ( 𝑔 ( ·𝑠 ‘ 𝐶 ) 𝐺 ) 𝑅 𝑧 ) ) → 𝑡 = ( ( 𝑔 ( ·𝑠 ‘ 𝐶 ) 𝐺 ) 𝑅 𝑧 ) )
45 eldifsni ⊢ ( 𝑋 ∈ ( 𝑉 ∖ { 0 } ) → 𝑋 ≠ 0 )
46 13 45 syl ⊢ ( 𝜑 → 𝑋 ≠ 0 )
47 46 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( ( 𝑀 ‘ ( 𝑁 ‘ { 𝑋 } ) ) ( LSSum ‘ 𝐶 ) ( 𝑀 ‘ ( 𝑁 ‘ { 𝑌 } ) ) ) ∧ ( 𝑀 ‘ ( 𝑁 ‘ { ( 𝑋 − 𝑌 ) } ) ) = ( 𝐽 ‘ { 𝑡 } ) ) → 𝑋 ≠ 0 )
48 47 3ad2ant1 ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ ( ( 𝑀 ‘ ( 𝑁 ‘ { 𝑋 } ) ) ( LSSum ‘ 𝐶 ) ( 𝑀 ‘ ( 𝑁 ‘ { 𝑌 } ) ) ) ∧ ( 𝑀 ‘ ( 𝑁 ‘ { ( 𝑋 − 𝑌 ) } ) ) = ( 𝐽 ‘ { 𝑡 } ) ) ∧ ( 𝑔 ∈ ( Base ‘ ( Scalar ‘ 𝑈 ) ) ∧ 𝑧 ∈ ( 𝑀 ‘ ( 𝑁 ‘ { 𝑌 } ) ) ) ∧ 𝑡 = ( ( 𝑔 ( ·𝑠 ‘ 𝐶 ) 𝐺 ) 𝑅 𝑧 ) ) → 𝑋 ≠ 0 )
49 eldifsni ⊢ ( 𝑌 ∈ ( 𝑉 ∖ { 0 } ) → 𝑌 ≠ 0 )
50 14 49 syl ⊢ ( 𝜑 → 𝑌 ≠ 0 )
51 50 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( ( 𝑀 ‘ ( 𝑁 ‘ { 𝑋 } ) ) ( LSSum ‘ 𝐶 ) ( 𝑀 ‘ ( 𝑁 ‘ { 𝑌 } ) ) ) ∧ ( 𝑀 ‘ ( 𝑁 ‘ { ( 𝑋 − 𝑌 ) } ) ) = ( 𝐽 ‘ { 𝑡 } ) ) → 𝑌 ≠ 0 )
52 51 3ad2ant1 ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ ( ( 𝑀 ‘ ( 𝑁 ‘ { 𝑋 } ) ) ( LSSum ‘ 𝐶 ) ( 𝑀 ‘ ( 𝑁 ‘ { 𝑌 } ) ) ) ∧ ( 𝑀 ‘ ( 𝑁 ‘ { ( 𝑋 − 𝑌 ) } ) ) = ( 𝐽 ‘ { 𝑡 } ) ) ∧ ( 𝑔 ∈ ( Base ‘ ( Scalar ‘ 𝑈 ) ) ∧ 𝑧 ∈ ( 𝑀 ‘ ( 𝑁 ‘ { 𝑌 } ) ) ) ∧ 𝑡 = ( ( 𝑔 ( ·𝑠 ‘ 𝐶 ) 𝐺 ) 𝑅 𝑧 ) ) → 𝑌 ≠ 0 )
53 eqid ⊢ ( ( ( invr ‘ ( Scalar ‘ 𝑈 ) ) ‘ 𝑔 ) ( ·𝑠 ‘ 𝐶 ) 𝑧 ) = ( ( ( invr ‘ ( Scalar ‘ 𝑈 ) ) ‘ 𝑔 ) ( ·𝑠 ‘ 𝐶 ) 𝑧 )
54 1 2 3 4 5 7 8 32 33 34 20 11 9 35 26 27 28 10 36 37 6 39 40 41 42 43 44 48 52 53 mapdpglem23 ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ ( ( 𝑀 ‘ ( 𝑁 ‘ { 𝑋 } ) ) ( LSSum ‘ 𝐶 ) ( 𝑀 ‘ ( 𝑁 ‘ { 𝑌 } ) ) ) ∧ ( 𝑀 ‘ ( 𝑁 ‘ { ( 𝑋 − 𝑌 ) } ) ) = ( 𝐽 ‘ { 𝑡 } ) ) ∧ ( 𝑔 ∈ ( Base ‘ ( Scalar ‘ 𝑈 ) ) ∧ 𝑧 ∈ ( 𝑀 ‘ ( 𝑁 ‘ { 𝑌 } ) ) ) ∧ 𝑡 = ( ( 𝑔 ( ·𝑠 ‘ 𝐶 ) 𝐺 ) 𝑅 𝑧 ) ) → ∃ ℎ ∈ 𝐹 ( ( 𝑀 ‘ ( 𝑁 ‘ { 𝑌 } ) ) = ( 𝐽 ‘ { ℎ } ) ∧ ( 𝑀 ‘ ( 𝑁 ‘ { ( 𝑋 − 𝑌 ) } ) ) = ( 𝐽 ‘ { ( 𝐺 𝑅 ℎ ) } ) ) )
55 54 3exp ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( ( 𝑀 ‘ ( 𝑁 ‘ { 𝑋 } ) ) ( LSSum ‘ 𝐶 ) ( 𝑀 ‘ ( 𝑁 ‘ { 𝑌 } ) ) ) ∧ ( 𝑀 ‘ ( 𝑁 ‘ { ( 𝑋 − 𝑌 ) } ) ) = ( 𝐽 ‘ { 𝑡 } ) ) → ( ( 𝑔 ∈ ( Base ‘ ( Scalar ‘ 𝑈 ) ) ∧ 𝑧 ∈ ( 𝑀 ‘ ( 𝑁 ‘ { 𝑌 } ) ) ) → ( 𝑡 = ( ( 𝑔 ( ·𝑠 ‘ 𝐶 ) 𝐺 ) 𝑅 𝑧 ) → ∃ ℎ ∈ 𝐹 ( ( 𝑀 ‘ ( 𝑁 ‘ { 𝑌 } ) ) = ( 𝐽 ‘ { ℎ } ) ∧ ( 𝑀 ‘ ( 𝑁 ‘ { ( 𝑋 − 𝑌 ) } ) ) = ( 𝐽 ‘ { ( 𝐺 𝑅 ℎ ) } ) ) ) ) )
56 55 rexlimdvv ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( ( 𝑀 ‘ ( 𝑁 ‘ { 𝑋 } ) ) ( LSSum ‘ 𝐶 ) ( 𝑀 ‘ ( 𝑁 ‘ { 𝑌 } ) ) ) ∧ ( 𝑀 ‘ ( 𝑁 ‘ { ( 𝑋 − 𝑌 ) } ) ) = ( 𝐽 ‘ { 𝑡 } ) ) → ( ∃ 𝑔 ∈ ( Base ‘ ( Scalar ‘ 𝑈 ) ) ∃ 𝑧 ∈ ( 𝑀 ‘ ( 𝑁 ‘ { 𝑌 } ) ) 𝑡 = ( ( 𝑔 ( ·𝑠 ‘ 𝐶 ) 𝐺 ) 𝑅 𝑧 ) → ∃ ℎ ∈ 𝐹 ( ( 𝑀 ‘ ( 𝑁 ‘ { 𝑌 } ) ) = ( 𝐽 ‘ { ℎ } ) ∧ ( 𝑀 ‘ ( 𝑁 ‘ { ( 𝑋 − 𝑌 ) } ) ) = ( 𝐽 ‘ { ( 𝐺 𝑅 ℎ ) } ) ) ) )
57 31 56 mpd ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( ( 𝑀 ‘ ( 𝑁 ‘ { 𝑋 } ) ) ( LSSum ‘ 𝐶 ) ( 𝑀 ‘ ( 𝑁 ‘ { 𝑌 } ) ) ) ∧ ( 𝑀 ‘ ( 𝑁 ‘ { ( 𝑋 − 𝑌 ) } ) ) = ( 𝐽 ‘ { 𝑡 } ) ) → ∃ ℎ ∈ 𝐹 ( ( 𝑀 ‘ ( 𝑁 ‘ { 𝑌 } ) ) = ( 𝐽 ‘ { ℎ } ) ∧ ( 𝑀 ‘ ( 𝑁 ‘ { ( 𝑋 − 𝑌 ) } ) ) = ( 𝐽 ‘ { ( 𝐺 𝑅 ℎ ) } ) ) )
58 57 rexlimdv3a ⊢ ( 𝜑 → ( ∃ 𝑡 ∈ ( ( 𝑀 ‘ ( 𝑁 ‘ { 𝑋 } ) ) ( LSSum ‘ 𝐶 ) ( 𝑀 ‘ ( 𝑁 ‘ { 𝑌 } ) ) ) ( 𝑀 ‘ ( 𝑁 ‘ { ( 𝑋 − 𝑌 ) } ) ) = ( 𝐽 ‘ { 𝑡 } ) → ∃ ℎ ∈ 𝐹 ( ( 𝑀 ‘ ( 𝑁 ‘ { 𝑌 } ) ) = ( 𝐽 ‘ { ℎ } ) ∧ ( 𝑀 ‘ ( 𝑁 ‘ { ( 𝑋 − 𝑌 ) } ) ) = ( 𝐽 ‘ { ( 𝐺 𝑅 ℎ ) } ) ) ) )
59 21 58 mpd ⊢ ( 𝜑 → ∃ ℎ ∈ 𝐹 ( ( 𝑀 ‘ ( 𝑁 ‘ { 𝑌 } ) ) = ( 𝐽 ‘ { ℎ } ) ∧ ( 𝑀 ‘ ( 𝑁 ‘ { ( 𝑋 − 𝑌 ) } ) ) = ( 𝐽 ‘ { ( 𝐺 𝑅 ℎ ) } ) ) )