Theorem hdmap11lem1

Description: Lemma for hdmapadd . (Contributed by NM, 26-May-2015)

	Ref	Expression
Hypotheses	hdmap11.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
	hdmap11.u	⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
	hdmap11.v	⊢ 𝑉 = ( Base ‘ 𝑈 )
	hdmap11.p	⊢ + = ( +g ‘ 𝑈 )
	hdmap11.c	⊢ 𝐶 = ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 )
	hdmap11.a	⊢ ✚ = ( +g ‘ 𝐶 )
	hdmap11.s	⊢ 𝑆 = ( ( HDMap ‘ 𝐾 ) ‘ 𝑊 )
	hdmap11.k	⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
	hdmap11.x	⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
	hdmap11.y	⊢ ( 𝜑 → 𝑌 ∈ 𝑉 )
	hdmap11.e	⊢ 𝐸 = ⟨ ( I ↾ ( Base ‘ 𝐾 ) ) , ( I ↾ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ) ⟩
	hdmap11.o	⊢ 0 = ( 0g ‘ 𝑈 )
	hdmap11.n	⊢ 𝑁 = ( LSpan ‘ 𝑈 )
	hdmap11.d	⊢ 𝐷 = ( Base ‘ 𝐶 )
	hdmap11.l	⊢ 𝐿 = ( LSpan ‘ 𝐶 )
	hdmap11.m	⊢ 𝑀 = ( ( mapd ‘ 𝐾 ) ‘ 𝑊 )
	hdmap11.j	⊢ 𝐽 = ( ( HVMap ‘ 𝐾 ) ‘ 𝑊 )
	hdmap11.i	⊢ 𝐼 = ( ( HDMap1 ‘ 𝐾 ) ‘ 𝑊 )
	hdmap11lem0.1a	⊢ ( 𝜑 → 𝑧 ∈ 𝑉 )
	hdmap11lem0.6	⊢ ( 𝜑 → ¬ 𝑧 ∈ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) )
	hdmap11lem0.2a	⊢ ( 𝜑 → ( 𝑁 ‘ { 𝑧 } ) ≠ ( 𝑁 ‘ { 𝐸 } ) )
Assertion	hdmap11lem1	⊢ ( 𝜑 → ( 𝑆 ‘ ( 𝑋 + 𝑌 ) ) = ( ( 𝑆 ‘ 𝑋 ) ✚ ( 𝑆 ‘ 𝑌 ) ) )

Proof

Step	Hyp	Ref	Expression
1		hdmap11.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
2		hdmap11.u	⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
3		hdmap11.v	⊢ 𝑉 = ( Base ‘ 𝑈 )
4		hdmap11.p	⊢ + = ( +g ‘ 𝑈 )
5		hdmap11.c	⊢ 𝐶 = ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 )
6		hdmap11.a	⊢ ✚ = ( +g ‘ 𝐶 )
7		hdmap11.s	⊢ 𝑆 = ( ( HDMap ‘ 𝐾 ) ‘ 𝑊 )
8		hdmap11.k	⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
9		hdmap11.x	⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
10		hdmap11.y	⊢ ( 𝜑 → 𝑌 ∈ 𝑉 )
11		hdmap11.e	⊢ 𝐸 = ⟨ ( I ↾ ( Base ‘ 𝐾 ) ) , ( I ↾ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ) ⟩
12		hdmap11.o	⊢ 0 = ( 0g ‘ 𝑈 )
13		hdmap11.n	⊢ 𝑁 = ( LSpan ‘ 𝑈 )
14		hdmap11.d	⊢ 𝐷 = ( Base ‘ 𝐶 )
15		hdmap11.l	⊢ 𝐿 = ( LSpan ‘ 𝐶 )
16		hdmap11.m	⊢ 𝑀 = ( ( mapd ‘ 𝐾 ) ‘ 𝑊 )
17		hdmap11.j	⊢ 𝐽 = ( ( HVMap ‘ 𝐾 ) ‘ 𝑊 )
18		hdmap11.i	⊢ 𝐼 = ( ( HDMap1 ‘ 𝐾 ) ‘ 𝑊 )
19		hdmap11lem0.1a	⊢ ( 𝜑 → 𝑧 ∈ 𝑉 )
20		hdmap11lem0.6	⊢ ( 𝜑 → ¬ 𝑧 ∈ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) )
21		hdmap11lem0.2a	⊢ ( 𝜑 → ( 𝑁 ‘ { 𝑧 } ) ≠ ( 𝑁 ‘ { 𝐸 } ) )
22		eqid	⊢ ( 0g ‘ 𝐶 ) = ( 0g ‘ 𝐶 )
23		eqid	⊢ ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
24		eqid	⊢ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
25	1 23 24 2 3 12 11 8	dvheveccl	⊢ ( 𝜑 → 𝐸 ∈ ( 𝑉 ∖ { 0 } ) )
26	1 2 3 12 5 14 22 17 8 25	hvmapcl2	⊢ ( 𝜑 → ( 𝐽 ‘ 𝐸 ) ∈ ( 𝐷 ∖ { ( 0g ‘ 𝐶 ) } ) )
27	26	eldifad	⊢ ( 𝜑 → ( 𝐽 ‘ 𝐸 ) ∈ 𝐷 )
28	1 2 3 12 13 5 15 16 17 8 25	mapdhvmap	⊢ ( 𝜑 → ( 𝑀 ‘ ( 𝑁 ‘ { 𝐸 } ) ) = ( 𝐿 ‘ { ( 𝐽 ‘ 𝐸 ) } ) )
29	21	necomd	⊢ ( 𝜑 → ( 𝑁 ‘ { 𝐸 } ) ≠ ( 𝑁 ‘ { 𝑧 } ) )
30	1 2 3 12 13 5 14 15 16 18 8 27 28 29 25 19	hdmap1cl	⊢ ( 𝜑 → ( 𝐼 ‘ ⟨ 𝐸 , ( 𝐽 ‘ 𝐸 ) , 𝑧 ⟩ ) ∈ 𝐷 )
31		eqid	⊢ ( LSubSp ‘ 𝑈 ) = ( LSubSp ‘ 𝑈 )
32	1 2 8	dvhlmod	⊢ ( 𝜑 → 𝑈 ∈ LMod )
33	3 31 13 32 9 10	lspprcl	⊢ ( 𝜑 → ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ∈ ( LSubSp ‘ 𝑈 ) )
34	12 31 32 33 19 20	lssneln0	⊢ ( 𝜑 → 𝑧 ∈ ( 𝑉 ∖ { 0 } ) )
35		eqidd	⊢ ( 𝜑 → ( 𝐼 ‘ ⟨ 𝐸 , ( 𝐽 ‘ 𝐸 ) , 𝑧 ⟩ ) = ( 𝐼 ‘ ⟨ 𝐸 , ( 𝐽 ‘ 𝐸 ) , 𝑧 ⟩ ) )
36		eqid	⊢ ( -g ‘ 𝑈 ) = ( -g ‘ 𝑈 )
37		eqid	⊢ ( -g ‘ 𝐶 ) = ( -g ‘ 𝐶 )
38	1 2 3 36 12 13 5 14 37 15 16 18 8 25 27 34 30 29 28	hdmap1eq	⊢ ( 𝜑 → ( ( 𝐼 ‘ ⟨ 𝐸 , ( 𝐽 ‘ 𝐸 ) , 𝑧 ⟩ ) = ( 𝐼 ‘ ⟨ 𝐸 , ( 𝐽 ‘ 𝐸 ) , 𝑧 ⟩ ) ↔ ( ( 𝑀 ‘ ( 𝑁 ‘ { 𝑧 } ) ) = ( 𝐿 ‘ { ( 𝐼 ‘ ⟨ 𝐸 , ( 𝐽 ‘ 𝐸 ) , 𝑧 ⟩ ) } ) ∧ ( 𝑀 ‘ ( 𝑁 ‘ { ( 𝐸 ( -g ‘ 𝑈 ) 𝑧 ) } ) ) = ( 𝐿 ‘ { ( ( 𝐽 ‘ 𝐸 ) ( -g ‘ 𝐶 ) ( 𝐼 ‘ ⟨ 𝐸 , ( 𝐽 ‘ 𝐸 ) , 𝑧 ⟩ ) ) } ) ) ) )
39	35 38	mpbid	⊢ ( 𝜑 → ( ( 𝑀 ‘ ( 𝑁 ‘ { 𝑧 } ) ) = ( 𝐿 ‘ { ( 𝐼 ‘ ⟨ 𝐸 , ( 𝐽 ‘ 𝐸 ) , 𝑧 ⟩ ) } ) ∧ ( 𝑀 ‘ ( 𝑁 ‘ { ( 𝐸 ( -g ‘ 𝑈 ) 𝑧 ) } ) ) = ( 𝐿 ‘ { ( ( 𝐽 ‘ 𝐸 ) ( -g ‘ 𝐶 ) ( 𝐼 ‘ ⟨ 𝐸 , ( 𝐽 ‘ 𝐸 ) , 𝑧 ⟩ ) ) } ) ) )
40	39	simpld	⊢ ( 𝜑 → ( 𝑀 ‘ ( 𝑁 ‘ { 𝑧 } ) ) = ( 𝐿 ‘ { ( 𝐼 ‘ ⟨ 𝐸 , ( 𝐽 ‘ 𝐸 ) , 𝑧 ⟩ ) } ) )
41	1 2 3 4 12 13 5 14 6 15 16 18 8 30 34 9 10 20 40	hdmap1l6	⊢ ( 𝜑 → ( 𝐼 ‘ ⟨ 𝑧 , ( 𝐼 ‘ ⟨ 𝐸 , ( 𝐽 ‘ 𝐸 ) , 𝑧 ⟩ ) , ( 𝑋 + 𝑌 ) ⟩ ) = ( ( 𝐼 ‘ ⟨ 𝑧 , ( 𝐼 ‘ ⟨ 𝐸 , ( 𝐽 ‘ 𝐸 ) , 𝑧 ⟩ ) , 𝑋 ⟩ ) ✚ ( 𝐼 ‘ ⟨ 𝑧 , ( 𝐼 ‘ ⟨ 𝐸 , ( 𝐽 ‘ 𝐸 ) , 𝑧 ⟩ ) , 𝑌 ⟩ ) ) )
42	3 4	lmodvacl	⊢ ( ( 𝑈 ∈ LMod ∧ 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) → ( 𝑋 + 𝑌 ) ∈ 𝑉 )
43	32 9 10 42	syl3anc	⊢ ( 𝜑 → ( 𝑋 + 𝑌 ) ∈ 𝑉 )
44	1 2 8	dvhlvec	⊢ ( 𝜑 → 𝑈 ∈ LVec )
45	25	eldifad	⊢ ( 𝜑 → 𝐸 ∈ 𝑉 )
46	3 4 13 32 9 10	lspprvacl	⊢ ( 𝜑 → ( 𝑋 + 𝑌 ) ∈ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) )
47	31 13 32 33 46	ellspsn5	⊢ ( 𝜑 → ( 𝑁 ‘ { ( 𝑋 + 𝑌 ) } ) ⊆ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) )
48	47 20	ssneldd	⊢ ( 𝜑 → ¬ 𝑧 ∈ ( 𝑁 ‘ { ( 𝑋 + 𝑌 ) } ) )
49	3 13 32 19 43 48	lspsnne2	⊢ ( 𝜑 → ( 𝑁 ‘ { 𝑧 } ) ≠ ( 𝑁 ‘ { ( 𝑋 + 𝑌 ) } ) )
50	3 13 12 44 45 43 34 21 49	hdmaplem4	⊢ ( 𝜑 → ¬ 𝑧 ∈ ( ( 𝑁 ‘ { 𝐸 } ) ∪ ( 𝑁 ‘ { ( 𝑋 + 𝑌 ) } ) ) )
51	1 11 2 3 13 5 14 17 18 7 8 43 19 50	hdmapval2	⊢ ( 𝜑 → ( 𝑆 ‘ ( 𝑋 + 𝑌 ) ) = ( 𝐼 ‘ ⟨ 𝑧 , ( 𝐼 ‘ ⟨ 𝐸 , ( 𝐽 ‘ 𝐸 ) , 𝑧 ⟩ ) , ( 𝑋 + 𝑌 ) ⟩ ) )
52	3 13 44 19 9 10 20	lspindpi	⊢ ( 𝜑 → ( ( 𝑁 ‘ { 𝑧 } ) ≠ ( 𝑁 ‘ { 𝑋 } ) ∧ ( 𝑁 ‘ { 𝑧 } ) ≠ ( 𝑁 ‘ { 𝑌 } ) ) )
53	52	simpld	⊢ ( 𝜑 → ( 𝑁 ‘ { 𝑧 } ) ≠ ( 𝑁 ‘ { 𝑋 } ) )
54	3 13 12 44 45 9 34 21 53	hdmaplem4	⊢ ( 𝜑 → ¬ 𝑧 ∈ ( ( 𝑁 ‘ { 𝐸 } ) ∪ ( 𝑁 ‘ { 𝑋 } ) ) )
55	1 11 2 3 13 5 14 17 18 7 8 9 19 54	hdmapval2	⊢ ( 𝜑 → ( 𝑆 ‘ 𝑋 ) = ( 𝐼 ‘ ⟨ 𝑧 , ( 𝐼 ‘ ⟨ 𝐸 , ( 𝐽 ‘ 𝐸 ) , 𝑧 ⟩ ) , 𝑋 ⟩ ) )
56	52	simprd	⊢ ( 𝜑 → ( 𝑁 ‘ { 𝑧 } ) ≠ ( 𝑁 ‘ { 𝑌 } ) )
57	3 13 12 44 45 10 34 21 56	hdmaplem4	⊢ ( 𝜑 → ¬ 𝑧 ∈ ( ( 𝑁 ‘ { 𝐸 } ) ∪ ( 𝑁 ‘ { 𝑌 } ) ) )
58	1 11 2 3 13 5 14 17 18 7 8 10 19 57	hdmapval2	⊢ ( 𝜑 → ( 𝑆 ‘ 𝑌 ) = ( 𝐼 ‘ ⟨ 𝑧 , ( 𝐼 ‘ ⟨ 𝐸 , ( 𝐽 ‘ 𝐸 ) , 𝑧 ⟩ ) , 𝑌 ⟩ ) )
59	55 58	oveq12d	⊢ ( 𝜑 → ( ( 𝑆 ‘ 𝑋 ) ✚ ( 𝑆 ‘ 𝑌 ) ) = ( ( 𝐼 ‘ ⟨ 𝑧 , ( 𝐼 ‘ ⟨ 𝐸 , ( 𝐽 ‘ 𝐸 ) , 𝑧 ⟩ ) , 𝑋 ⟩ ) ✚ ( 𝐼 ‘ ⟨ 𝑧 , ( 𝐼 ‘ ⟨ 𝐸 , ( 𝐽 ‘ 𝐸 ) , 𝑧 ⟩ ) , 𝑌 ⟩ ) ) )
60	41 51 59	3eqtr4d	⊢ ( 𝜑 → ( 𝑆 ‘ ( 𝑋 + 𝑌 ) ) = ( ( 𝑆 ‘ 𝑋 ) ✚ ( 𝑆 ‘ 𝑌 ) ) )