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	⊢ ( 𝜑 → ∃ ℎ ∈ 𝐹 ( ( 𝑀 ‘ ( 𝑁 ‘ { 𝑌 } ) ) = ( 𝐽 ‘ { ℎ } ) ∧ ( 𝑀 ‘ ( 𝑁 ‘ { ( 𝑋 − 𝑌 ) } ) ) = ( 𝐽 ‘ { ( 𝐺 𝑅 ℎ ) } ) ) )