hdmap11lem2 - Mathbox for Norm Megill

	Mathbox for Norm Megill		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > hdmap11lem2		Structured version Visualization version GIF version

Theorem hdmap11lem2 41824

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

**Hypotheses**
Ref	Expression
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 = (0_g‘𝑈)
hdmap11.n	⊢ 𝑁 = (LSpan‘𝑈)
hdmap11.d	⊢ 𝐷 = (Base‘𝐶)
hdmap11.l	⊢ 𝐿 = (LSpan‘𝐶)
hdmap11.m	⊢ 𝑀 = ((mapd‘𝐾)‘𝑊)
hdmap11.j	⊢ 𝐽 = ((HVMap‘𝐾)‘𝑊)
hdmap11.i	⊢ 𝐼 = ((HDMap1‘𝐾)‘𝑊)

**Assertion**
Ref	Expression
hdmap11lem2	⊢ (𝜑 → (𝑆‘(𝑋 + 𝑌)) = ((𝑆‘𝑋) ✚ (𝑆‘𝑌)))

Proof of Theorem hdmap11lem2 Dummy variable 𝑧 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		hdmap11.h	. . . . . 6 ⊢ 𝐻 = (LHyp‘𝐾)
2		hdmap11.u	. . . . . 6 ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)
3		hdmap11.v	. . . . . 6 ⊢ 𝑉 = (Base‘𝑈)
4		hdmap11.n	. . . . . 6 ⊢ 𝑁 = (LSpan‘𝑈)
5		hdmap11.k	. . . . . 6 ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))
6		hdmap11.x	. . . . . 6 ⊢ (𝜑 → 𝑋 ∈ 𝑉)
7		hdmap11.y	. . . . . 6 ⊢ (𝜑 → 𝑌 ∈ 𝑉)
8	1, 2, 3, 4, 5, 6, 7	dvh3dim 41428	. . . . 5 ⊢ (𝜑 → ∃𝑧 ∈ 𝑉 ¬ 𝑧 ∈ (𝑁‘{𝑋, 𝑌}))
9	8	adantr 480	. . . 4 ⊢ ((𝜑 ∧ 𝐸 ∈ (𝑁‘{𝑋, 𝑌})) → ∃𝑧 ∈ 𝑉 ¬ 𝑧 ∈ (𝑁‘{𝑋, 𝑌}))
10		eqid 2729	. . . . . . . 8 ⊢ (LSubSp‘𝑈) = (LSubSp‘𝑈)
11	1, 2, 5	dvhlmod 41092	. . . . . . . . 9 ⊢ (𝜑 → 𝑈 ∈ LMod)
12	11	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝐸 ∈ (𝑁‘{𝑋, 𝑌})) → 𝑈 ∈ LMod)
13	3, 10, 4, 11, 6, 7	lspprcl 20899	. . . . . . . . 9 ⊢ (𝜑 → (𝑁‘{𝑋, 𝑌}) ∈ (LSubSp‘𝑈))
14	13	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝐸 ∈ (𝑁‘{𝑋, 𝑌})) → (𝑁‘{𝑋, 𝑌}) ∈ (LSubSp‘𝑈))
15		simpr 484	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝐸 ∈ (𝑁‘{𝑋, 𝑌})) → 𝐸 ∈ (𝑁‘{𝑋, 𝑌}))
16	10, 4, 12, 14, 15	ellspsn5 20917	. . . . . . 7 ⊢ ((𝜑 ∧ 𝐸 ∈ (𝑁‘{𝑋, 𝑌})) → (𝑁‘{𝐸}) ⊆ (𝑁‘{𝑋, 𝑌}))
17	16	ssneld 3939	. . . . . 6 ⊢ ((𝜑 ∧ 𝐸 ∈ (𝑁‘{𝑋, 𝑌})) → (¬ 𝑧 ∈ (𝑁‘{𝑋, 𝑌}) → ¬ 𝑧 ∈ (𝑁‘{𝐸})))
18	17	ancld 550	. . . . 5 ⊢ ((𝜑 ∧ 𝐸 ∈ (𝑁‘{𝑋, 𝑌})) → (¬ 𝑧 ∈ (𝑁‘{𝑋, 𝑌}) → (¬ 𝑧 ∈ (𝑁‘{𝑋, 𝑌}) ∧ ¬ 𝑧 ∈ (𝑁‘{𝐸}))))
19	18	reximdv 3144	. . . 4 ⊢ ((𝜑 ∧ 𝐸 ∈ (𝑁‘{𝑋, 𝑌})) → (∃𝑧 ∈ 𝑉 ¬ 𝑧 ∈ (𝑁‘{𝑋, 𝑌}) → ∃𝑧 ∈ 𝑉 (¬ 𝑧 ∈ (𝑁‘{𝑋, 𝑌}) ∧ ¬ 𝑧 ∈ (𝑁‘{𝐸}))))
20	9, 19	mpd 15	. . 3 ⊢ ((𝜑 ∧ 𝐸 ∈ (𝑁‘{𝑋, 𝑌})) → ∃𝑧 ∈ 𝑉 (¬ 𝑧 ∈ (𝑁‘{𝑋, 𝑌}) ∧ ¬ 𝑧 ∈ (𝑁‘{𝐸})))
21		eqid 2729	. . . . . . . . . 10 ⊢ (Base‘𝐾) = (Base‘𝐾)
22		eqid 2729	. . . . . . . . . 10 ⊢ ((LTrn‘𝐾)‘𝑊) = ((LTrn‘𝐾)‘𝑊)
23		hdmap11.o	. . . . . . . . . 10 ⊢ 0 = (0_g‘𝑈)
24		hdmap11.e	. . . . . . . . . 10 ⊢ 𝐸 = ⟨( I ↾ (Base‘𝐾)), ( I ↾ ((LTrn‘𝐾)‘𝑊))⟩
25	1, 21, 22, 2, 3, 23, 24, 5	dvheveccl 41094	. . . . . . . . 9 ⊢ (𝜑 → 𝐸 ∈ (𝑉 ∖ { 0 }))
26	25	eldifad 3917	. . . . . . . 8 ⊢ (𝜑 → 𝐸 ∈ 𝑉)
27	1, 2, 3, 4, 5, 26, 7	dvh3dim 41428	. . . . . . 7 ⊢ (𝜑 → ∃𝑧 ∈ 𝑉 ¬ 𝑧 ∈ (𝑁‘{𝐸, 𝑌}))
28	27	adantr 480	. . . . . 6 ⊢ ((𝜑 ∧ 𝑋 = 0 ) → ∃𝑧 ∈ 𝑉 ¬ 𝑧 ∈ (𝑁‘{𝐸, 𝑌}))
29		preq1 4687	. . . . . . . . . . . . 13 ⊢ (𝑋 = 0 → {𝑋, 𝑌} = { 0 , 𝑌})
30		prcom 4686	. . . . . . . . . . . . 13 ⊢ { 0 , 𝑌} = {𝑌, 0 }
31	29, 30	eqtrdi 2780	. . . . . . . . . . . 12 ⊢ (𝑋 = 0 → {𝑋, 𝑌} = {𝑌, 0 })
32	31	fveq2d 6830	. . . . . . . . . . 11 ⊢ (𝑋 = 0 → (𝑁‘{𝑋, 𝑌}) = (𝑁‘{𝑌, 0 }))
33	3, 23, 4, 11, 7	lsppr0 21014	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑁‘{𝑌, 0 }) = (𝑁‘{𝑌}))
34	32, 33	sylan9eqr 2786	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑋 = 0 ) → (𝑁‘{𝑋, 𝑌}) = (𝑁‘{𝑌}))
35	3, 10, 4, 11, 26, 7	lspprcl 20899	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑁‘{𝐸, 𝑌}) ∈ (LSubSp‘𝑈))
36	3, 4, 11, 26, 7	lspprid2 20919	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑌 ∈ (𝑁‘{𝐸, 𝑌}))
37	10, 4, 11, 35, 36	ellspsn5 20917	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑁‘{𝑌}) ⊆ (𝑁‘{𝐸, 𝑌}))
38	37	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑋 = 0 ) → (𝑁‘{𝑌}) ⊆ (𝑁‘{𝐸, 𝑌}))
39	34, 38	eqsstrd 3972	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑋 = 0 ) → (𝑁‘{𝑋, 𝑌}) ⊆ (𝑁‘{𝐸, 𝑌}))
40	39	ssneld 3939	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑋 = 0 ) → (¬ 𝑧 ∈ (𝑁‘{𝐸, 𝑌}) → ¬ 𝑧 ∈ (𝑁‘{𝑋, 𝑌})))
41	3, 4, 11, 26, 7	lspprid1 20918	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐸 ∈ (𝑁‘{𝐸, 𝑌}))
42	10, 4, 11, 35, 41	ellspsn5 20917	. . . . . . . . . 10 ⊢ (𝜑 → (𝑁‘{𝐸}) ⊆ (𝑁‘{𝐸, 𝑌}))
43	42	adantr 480	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑋 = 0 ) → (𝑁‘{𝐸}) ⊆ (𝑁‘{𝐸, 𝑌}))
44	43	ssneld 3939	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑋 = 0 ) → (¬ 𝑧 ∈ (𝑁‘{𝐸, 𝑌}) → ¬ 𝑧 ∈ (𝑁‘{𝐸})))
45	40, 44	jcad 512	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑋 = 0 ) → (¬ 𝑧 ∈ (𝑁‘{𝐸, 𝑌}) → (¬ 𝑧 ∈ (𝑁‘{𝑋, 𝑌}) ∧ ¬ 𝑧 ∈ (𝑁‘{𝐸}))))
46	45	reximdv 3144	. . . . . 6 ⊢ ((𝜑 ∧ 𝑋 = 0 ) → (∃𝑧 ∈ 𝑉 ¬ 𝑧 ∈ (𝑁‘{𝐸, 𝑌}) → ∃𝑧 ∈ 𝑉 (¬ 𝑧 ∈ (𝑁‘{𝑋, 𝑌}) ∧ ¬ 𝑧 ∈ (𝑁‘{𝐸}))))
47	28, 46	mpd 15	. . . . 5 ⊢ ((𝜑 ∧ 𝑋 = 0 ) → ∃𝑧 ∈ 𝑉 (¬ 𝑧 ∈ (𝑁‘{𝑋, 𝑌}) ∧ ¬ 𝑧 ∈ (𝑁‘{𝐸})))
48	47	adantlr 715	. . . 4 ⊢ (((𝜑 ∧ ¬ 𝐸 ∈ (𝑁‘{𝑋, 𝑌})) ∧ 𝑋 = 0 ) → ∃𝑧 ∈ 𝑉 (¬ 𝑧 ∈ (𝑁‘{𝑋, 𝑌}) ∧ ¬ 𝑧 ∈ (𝑁‘{𝐸})))
49		hdmap11.p	. . . . . . . 8 ⊢ + = (+_g‘𝑈)
50	3, 49	lmodvacl 20796	. . . . . . 7 ⊢ ((𝑈 ∈ LMod ∧ 𝐸 ∈ 𝑉 ∧ 𝑋 ∈ 𝑉) → (𝐸 + 𝑋) ∈ 𝑉)
51	11, 26, 6, 50	syl3anc 1373	. . . . . 6 ⊢ (𝜑 → (𝐸 + 𝑋) ∈ 𝑉)
52	51	ad2antrr 726	. . . . 5 ⊢ (((𝜑 ∧ ¬ 𝐸 ∈ (𝑁‘{𝑋, 𝑌})) ∧ 𝑋 ≠ 0 ) → (𝐸 + 𝑋) ∈ 𝑉)
53	11	ad2antrr 726	. . . . . 6 ⊢ (((𝜑 ∧ ¬ 𝐸 ∈ (𝑁‘{𝑋, 𝑌})) ∧ 𝑋 ≠ 0 ) → 𝑈 ∈ LMod)
54	13	ad2antrr 726	. . . . . 6 ⊢ (((𝜑 ∧ ¬ 𝐸 ∈ (𝑁‘{𝑋, 𝑌})) ∧ 𝑋 ≠ 0 ) → (𝑁‘{𝑋, 𝑌}) ∈ (LSubSp‘𝑈))
55	3, 4, 11, 6, 7	lspprid1 20918	. . . . . . 7 ⊢ (𝜑 → 𝑋 ∈ (𝑁‘{𝑋, 𝑌}))
56	55	ad2antrr 726	. . . . . 6 ⊢ (((𝜑 ∧ ¬ 𝐸 ∈ (𝑁‘{𝑋, 𝑌})) ∧ 𝑋 ≠ 0 ) → 𝑋 ∈ (𝑁‘{𝑋, 𝑌}))
57	26	ad2antrr 726	. . . . . 6 ⊢ (((𝜑 ∧ ¬ 𝐸 ∈ (𝑁‘{𝑋, 𝑌})) ∧ 𝑋 ≠ 0 ) → 𝐸 ∈ 𝑉)
58		simplr 768	. . . . . 6 ⊢ (((𝜑 ∧ ¬ 𝐸 ∈ (𝑁‘{𝑋, 𝑌})) ∧ 𝑋 ≠ 0 ) → ¬ 𝐸 ∈ (𝑁‘{𝑋, 𝑌}))
59	3, 49, 10, 53, 54, 56, 57, 58	lssvancl2 20867	. . . . 5 ⊢ (((𝜑 ∧ ¬ 𝐸 ∈ (𝑁‘{𝑋, 𝑌})) ∧ 𝑋 ≠ 0 ) → ¬ (𝐸 + 𝑋) ∈ (𝑁‘{𝑋, 𝑌}))
60	3, 10, 4	lspsncl 20898	. . . . . . . 8 ⊢ ((𝑈 ∈ LMod ∧ 𝐸 ∈ 𝑉) → (𝑁‘{𝐸}) ∈ (LSubSp‘𝑈))
61	11, 26, 60	syl2anc 584	. . . . . . 7 ⊢ (𝜑 → (𝑁‘{𝐸}) ∈ (LSubSp‘𝑈))
62	61	ad2antrr 726	. . . . . 6 ⊢ (((𝜑 ∧ ¬ 𝐸 ∈ (𝑁‘{𝑋, 𝑌})) ∧ 𝑋 ≠ 0 ) → (𝑁‘{𝐸}) ∈ (LSubSp‘𝑈))
63	3, 4	lspsnid 20914	. . . . . . . 8 ⊢ ((𝑈 ∈ LMod ∧ 𝐸 ∈ 𝑉) → 𝐸 ∈ (𝑁‘{𝐸}))
64	11, 26, 63	syl2anc 584	. . . . . . 7 ⊢ (𝜑 → 𝐸 ∈ (𝑁‘{𝐸}))
65	64	ad2antrr 726	. . . . . 6 ⊢ (((𝜑 ∧ ¬ 𝐸 ∈ (𝑁‘{𝑋, 𝑌})) ∧ 𝑋 ≠ 0 ) → 𝐸 ∈ (𝑁‘{𝐸}))
66	6	ad2antrr 726	. . . . . 6 ⊢ (((𝜑 ∧ ¬ 𝐸 ∈ (𝑁‘{𝑋, 𝑌})) ∧ 𝑋 ≠ 0 ) → 𝑋 ∈ 𝑉)
67	1, 2, 5	dvhlvec 41091	. . . . . . . 8 ⊢ (𝜑 → 𝑈 ∈ LVec)
68	67	ad2antrr 726	. . . . . . 7 ⊢ (((𝜑 ∧ ¬ 𝐸 ∈ (𝑁‘{𝑋, 𝑌})) ∧ 𝑋 ≠ 0 ) → 𝑈 ∈ LVec)
69		simpr 484	. . . . . . . 8 ⊢ (((𝜑 ∧ ¬ 𝐸 ∈ (𝑁‘{𝑋, 𝑌})) ∧ 𝑋 ≠ 0 ) → 𝑋 ≠ 0 )
70		eldifsn 4740	. . . . . . . 8 ⊢ (𝑋 ∈ (𝑉 ∖ { 0 }) ↔ (𝑋 ∈ 𝑉 ∧ 𝑋 ≠ 0 ))
71	66, 69, 70	sylanbrc 583	. . . . . . 7 ⊢ (((𝜑 ∧ ¬ 𝐸 ∈ (𝑁‘{𝑋, 𝑌})) ∧ 𝑋 ≠ 0 ) → 𝑋 ∈ (𝑉 ∖ { 0 }))
72	10, 4, 11, 13, 55	ellspsn5 20917	. . . . . . . . . 10 ⊢ (𝜑 → (𝑁‘{𝑋}) ⊆ (𝑁‘{𝑋, 𝑌}))
73	72	sseld 3936	. . . . . . . . 9 ⊢ (𝜑 → (𝐸 ∈ (𝑁‘{𝑋}) → 𝐸 ∈ (𝑁‘{𝑋, 𝑌})))
74	73	con3dimp 408	. . . . . . . 8 ⊢ ((𝜑 ∧ ¬ 𝐸 ∈ (𝑁‘{𝑋, 𝑌})) → ¬ 𝐸 ∈ (𝑁‘{𝑋}))
75	74	adantr 480	. . . . . . 7 ⊢ (((𝜑 ∧ ¬ 𝐸 ∈ (𝑁‘{𝑋, 𝑌})) ∧ 𝑋 ≠ 0 ) → ¬ 𝐸 ∈ (𝑁‘{𝑋}))
76	3, 23, 4, 68, 57, 71, 75	lspsnnecom 21044	. . . . . 6 ⊢ (((𝜑 ∧ ¬ 𝐸 ∈ (𝑁‘{𝑋, 𝑌})) ∧ 𝑋 ≠ 0 ) → ¬ 𝑋 ∈ (𝑁‘{𝐸}))
77	3, 49, 10, 53, 62, 65, 66, 76	lssvancl1 20866	. . . . 5 ⊢ (((𝜑 ∧ ¬ 𝐸 ∈ (𝑁‘{𝑋, 𝑌})) ∧ 𝑋 ≠ 0 ) → ¬ (𝐸 + 𝑋) ∈ (𝑁‘{𝐸}))
78		eleq1 2816	. . . . . . . 8 ⊢ (𝑧 = (𝐸 + 𝑋) → (𝑧 ∈ (𝑁‘{𝑋, 𝑌}) ↔ (𝐸 + 𝑋) ∈ (𝑁‘{𝑋, 𝑌})))
79	78	notbid 318	. . . . . . 7 ⊢ (𝑧 = (𝐸 + 𝑋) → (¬ 𝑧 ∈ (𝑁‘{𝑋, 𝑌}) ↔ ¬ (𝐸 + 𝑋) ∈ (𝑁‘{𝑋, 𝑌})))
80		eleq1 2816	. . . . . . . 8 ⊢ (𝑧 = (𝐸 + 𝑋) → (𝑧 ∈ (𝑁‘{𝐸}) ↔ (𝐸 + 𝑋) ∈ (𝑁‘{𝐸})))
81	80	notbid 318	. . . . . . 7 ⊢ (𝑧 = (𝐸 + 𝑋) → (¬ 𝑧 ∈ (𝑁‘{𝐸}) ↔ ¬ (𝐸 + 𝑋) ∈ (𝑁‘{𝐸})))
82	79, 81	anbi12d 632	. . . . . 6 ⊢ (𝑧 = (𝐸 + 𝑋) → ((¬ 𝑧 ∈ (𝑁‘{𝑋, 𝑌}) ∧ ¬ 𝑧 ∈ (𝑁‘{𝐸})) ↔ (¬ (𝐸 + 𝑋) ∈ (𝑁‘{𝑋, 𝑌}) ∧ ¬ (𝐸 + 𝑋) ∈ (𝑁‘{𝐸}))))
83	82	rspcev 3579	. . . . 5 ⊢ (((𝐸 + 𝑋) ∈ 𝑉 ∧ (¬ (𝐸 + 𝑋) ∈ (𝑁‘{𝑋, 𝑌}) ∧ ¬ (𝐸 + 𝑋) ∈ (𝑁‘{𝐸}))) → ∃𝑧 ∈ 𝑉 (¬ 𝑧 ∈ (𝑁‘{𝑋, 𝑌}) ∧ ¬ 𝑧 ∈ (𝑁‘{𝐸})))
84	52, 59, 77, 83	syl12anc 836	. . . 4 ⊢ (((𝜑 ∧ ¬ 𝐸 ∈ (𝑁‘{𝑋, 𝑌})) ∧ 𝑋 ≠ 0 ) → ∃𝑧 ∈ 𝑉 (¬ 𝑧 ∈ (𝑁‘{𝑋, 𝑌}) ∧ ¬ 𝑧 ∈ (𝑁‘{𝐸})))
85	48, 84	pm2.61dane 3012	. . 3 ⊢ ((𝜑 ∧ ¬ 𝐸 ∈ (𝑁‘{𝑋, 𝑌})) → ∃𝑧 ∈ 𝑉 (¬ 𝑧 ∈ (𝑁‘{𝑋, 𝑌}) ∧ ¬ 𝑧 ∈ (𝑁‘{𝐸})))
86	20, 85	pm2.61dan 812	. 2 ⊢ (𝜑 → ∃𝑧 ∈ 𝑉 (¬ 𝑧 ∈ (𝑁‘{𝑋, 𝑌}) ∧ ¬ 𝑧 ∈ (𝑁‘{𝐸})))
87		hdmap11.c	. . . 4 ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊)
88		hdmap11.a	. . . 4 ⊢ ✚ = (+_g‘𝐶)
89		hdmap11.s	. . . 4 ⊢ 𝑆 = ((HDMap‘𝐾)‘𝑊)
90	5	3ad2ant1 1133	. . . 4 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑉 ∧ (¬ 𝑧 ∈ (𝑁‘{𝑋, 𝑌}) ∧ ¬ 𝑧 ∈ (𝑁‘{𝐸}))) → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))
91	6	3ad2ant1 1133	. . . 4 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑉 ∧ (¬ 𝑧 ∈ (𝑁‘{𝑋, 𝑌}) ∧ ¬ 𝑧 ∈ (𝑁‘{𝐸}))) → 𝑋 ∈ 𝑉)
92	7	3ad2ant1 1133	. . . 4 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑉 ∧ (¬ 𝑧 ∈ (𝑁‘{𝑋, 𝑌}) ∧ ¬ 𝑧 ∈ (𝑁‘{𝐸}))) → 𝑌 ∈ 𝑉)
93		hdmap11.d	. . . 4 ⊢ 𝐷 = (Base‘𝐶)
94		hdmap11.l	. . . 4 ⊢ 𝐿 = (LSpan‘𝐶)
95		hdmap11.m	. . . 4 ⊢ 𝑀 = ((mapd‘𝐾)‘𝑊)
96		hdmap11.j	. . . 4 ⊢ 𝐽 = ((HVMap‘𝐾)‘𝑊)
97		hdmap11.i	. . . 4 ⊢ 𝐼 = ((HDMap1‘𝐾)‘𝑊)
98		simp2 1137	. . . 4 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑉 ∧ (¬ 𝑧 ∈ (𝑁‘{𝑋, 𝑌}) ∧ ¬ 𝑧 ∈ (𝑁‘{𝐸}))) → 𝑧 ∈ 𝑉)
99		simp3l 1202	. . . 4 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑉 ∧ (¬ 𝑧 ∈ (𝑁‘{𝑋, 𝑌}) ∧ ¬ 𝑧 ∈ (𝑁‘{𝐸}))) → ¬ 𝑧 ∈ (𝑁‘{𝑋, 𝑌}))
100	11	3ad2ant1 1133	. . . . 5 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑉 ∧ (¬ 𝑧 ∈ (𝑁‘{𝑋, 𝑌}) ∧ ¬ 𝑧 ∈ (𝑁‘{𝐸}))) → 𝑈 ∈ LMod)
101	26	3ad2ant1 1133	. . . . 5 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑉 ∧ (¬ 𝑧 ∈ (𝑁‘{𝑋, 𝑌}) ∧ ¬ 𝑧 ∈ (𝑁‘{𝐸}))) → 𝐸 ∈ 𝑉)
102		simp3r 1203	. . . . 5 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑉 ∧ (¬ 𝑧 ∈ (𝑁‘{𝑋, 𝑌}) ∧ ¬ 𝑧 ∈ (𝑁‘{𝐸}))) → ¬ 𝑧 ∈ (𝑁‘{𝐸}))
103	3, 4, 100, 98, 101, 102	lspsnne2 21043	. . . 4 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑉 ∧ (¬ 𝑧 ∈ (𝑁‘{𝑋, 𝑌}) ∧ ¬ 𝑧 ∈ (𝑁‘{𝐸}))) → (𝑁‘{𝑧}) ≠ (𝑁‘{𝐸}))
104	1, 2, 3, 49, 87, 88, 89, 90, 91, 92, 24, 23, 4, 93, 94, 95, 96, 97, 98, 99, 103	hdmap11lem1 41823	. . 3 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑉 ∧ (¬ 𝑧 ∈ (𝑁‘{𝑋, 𝑌}) ∧ ¬ 𝑧 ∈ (𝑁‘{𝐸}))) → (𝑆‘(𝑋 + 𝑌)) = ((𝑆‘𝑋) ✚ (𝑆‘𝑌)))
105	104	rexlimdv3a 3134	. 2 ⊢ (𝜑 → (∃𝑧 ∈ 𝑉 (¬ 𝑧 ∈ (𝑁‘{𝑋, 𝑌}) ∧ ¬ 𝑧 ∈ (𝑁‘{𝐸})) → (𝑆‘(𝑋 + 𝑌)) = ((𝑆‘𝑋) ✚ (𝑆‘𝑌))))
106	86, 105	mpd 15	1 ⊢ (𝜑 → (𝑆‘(𝑋 + 𝑌)) = ((𝑆‘𝑋) ✚ (𝑆‘𝑌)))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ∧ wa 395 ∧ w3a 1086 = wceq 1540 ∈ wcel 2109 ≠ wne 2925 ∃wrex 3053 ∖ cdif 3902 ⊆ wss 3905 {csn 4579 {cpr 4581 ⟨cop 4585 I cid 5517 ↾ cres 5625 ‘cfv 6486 (class class class)co 7353 Basecbs 17138 +_gcplusg 17179 0_gc0g 17361 LModclmod 20781 LSubSpclss 20852 LSpanclspn 20892 LVecclvec 21024 HLchlt 39331 LHypclh 39966 LTrncltrn 40083 DVecHcdvh 41060 LCDualclcd 41568 mapdcmpd 41606 HVMapchvm 41738 HDMap1chdma1 41773 HDMapchdma 41774

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2008 ax-8 2111 ax-9 2119 ax-10 2142 ax-11 2158 ax-12 2178 ax-ext 2701 ax-rep 5221 ax-sep 5238 ax-nul 5248 ax-pow 5307 ax-pr 5374 ax-un 7675 ax-cnex 11084 ax-resscn 11085 ax-1cn 11086 ax-icn 11087 ax-addcl 11088 ax-addrcl 11089 ax-mulcl 11090 ax-mulrcl 11091 ax-mulcom 11092 ax-addass 11093 ax-mulass 11094 ax-distr 11095 ax-i2m1 11096 ax-1ne0 11097 ax-1rid 11098 ax-rnegex 11099 ax-rrecex 11100 ax-cnre 11101 ax-pre-lttri 11102 ax-pre-lttrn 11103 ax-pre-ltadd 11104 ax-pre-mulgt0 11105 ax-riotaBAD 38934

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1543 df-fal 1553 df-ex 1780 df-nf 1784 df-sb 2066 df-mo 2533 df-eu 2562 df-clab 2708 df-cleq 2721 df-clel 2803 df-nfc 2878 df-ne 2926 df-nel 3030 df-ral 3045 df-rex 3054 df-rmo 3345 df-reu 3346 df-rab 3397 df-v 3440 df-sbc 3745 df-csb 3854 df-dif 3908 df-un 3910 df-in 3912 df-ss 3922 df-pss 3925 df-nul 4287 df-if 4479 df-pw 4555 df-sn 4580 df-pr 4582 df-tp 4584 df-op 4586 df-ot 4588 df-uni 4862 df-int 4900 df-iun 4946 df-iin 4947 df-br 5096 df-opab 5158 df-mpt 5177 df-tr 5203 df-id 5518 df-eprel 5523 df-po 5531 df-so 5532 df-fr 5576 df-we 5578 df-xp 5629 df-rel 5630 df-cnv 5631 df-co 5632 df-dm 5633 df-rn 5634 df-res 5635 df-ima 5636 df-pred 6253 df-ord 6314 df-on 6315 df-lim 6316 df-suc 6317 df-iota 6442 df-fun 6488 df-fn 6489 df-f 6490 df-f1 6491 df-fo 6492 df-f1o 6493 df-fv 6494 df-riota 7310 df-ov 7356 df-oprab 7357 df-mpo 7358 df-of 7617 df-om 7807 df-1st 7931 df-2nd 7932 df-tpos 8166 df-undef 8213 df-frecs 8221 df-wrecs 8252 df-recs 8301 df-rdg 8339 df-1o 8395 df-2o 8396 df-er 8632 df-map 8762 df-en 8880 df-dom 8881 df-sdom 8882 df-fin 8883 df-pnf 11170 df-mnf 11171 df-xr 11172 df-ltxr 11173 df-le 11174 df-sub 11367 df-neg 11368 df-nn 12147 df-2 12209 df-3 12210 df-4 12211 df-5 12212 df-6 12213 df-n0 12403 df-z 12490 df-uz 12754 df-fz 13429 df-struct 17076 df-sets 17093 df-slot 17111 df-ndx 17123 df-base 17139 df-ress 17160 df-plusg 17192 df-mulr 17193 df-sca 17195 df-vsca 17196 df-0g 17363 df-mre 17506 df-mrc 17507 df-acs 17509 df-proset 18218 df-poset 18237 df-plt 18252 df-lub 18268 df-glb 18269 df-join 18270 df-meet 18271 df-p0 18347 df-p1 18348 df-lat 18356 df-clat 18423 df-mgm 18532 df-sgrp 18611 df-mnd 18627 df-submnd 18676 df-grp 18833 df-minusg 18834 df-sbg 18835 df-subg 19020 df-cntz 19214 df-oppg 19243 df-lsm 19533 df-cmn 19679 df-abl 19680 df-mgp 20044 df-rng 20056 df-ur 20085 df-ring 20138 df-oppr 20240 df-dvdsr 20260 df-unit 20261 df-invr 20291 df-dvr 20304 df-nzr 20416 df-rlreg 20597 df-domn 20598 df-drng 20634 df-lmod 20783 df-lss 20853 df-lsp 20893 df-lvec 21025 df-lsatoms 38957 df-lshyp 38958 df-lcv 39000 df-lfl 39039 df-lkr 39067 df-ldual 39105 df-oposet 39157 df-ol 39159 df-oml 39160 df-covers 39247 df-ats 39248 df-atl 39279 df-cvlat 39303 df-hlat 39332 df-llines 39480 df-lplanes 39481 df-lvols 39482 df-lines 39483 df-psubsp 39485 df-pmap 39486 df-padd 39778 df-lhyp 39970 df-laut 39971 df-ldil 40086 df-ltrn 40087 df-trl 40141 df-tgrp 40725 df-tendo 40737 df-edring 40739 df-dveca 40985 df-disoa 41011 df-dvech 41061 df-dib 41121 df-dic 41155 df-dih 41211 df-doch 41330 df-djh 41377 df-lcdual 41569 df-mapd 41607 df-hvmap 41739 df-hdmap1 41775 df-hdmap 41776

This theorem is referenced by: hdmapadd 41825

W3C validator