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 39453

Description: Lemma for hdmapadd 39454. (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 39057	. . . . 5 ⊢ (𝜑 → ∃𝑧 ∈ 𝑉 ¬ 𝑧 ∈ (𝑁‘{𝑋, 𝑌}))
9	8	adantr 484	. . . 4 ⊢ ((𝜑 ∧ 𝐸 ∈ (𝑁‘{𝑋, 𝑌})) → ∃𝑧 ∈ 𝑉 ¬ 𝑧 ∈ (𝑁‘{𝑋, 𝑌}))
10		eqid 2758	. . . . . . . 8 ⊢ (LSubSp‘𝑈) = (LSubSp‘𝑈)
11	1, 2, 5	dvhlmod 38721	. . . . . . . . 9 ⊢ (𝜑 → 𝑈 ∈ LMod)
12	11	adantr 484	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝐸 ∈ (𝑁‘{𝑋, 𝑌})) → 𝑈 ∈ LMod)
13	3, 10, 4, 11, 6, 7	lspprcl 19832	. . . . . . . . 9 ⊢ (𝜑 → (𝑁‘{𝑋, 𝑌}) ∈ (LSubSp‘𝑈))
14	13	adantr 484	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝐸 ∈ (𝑁‘{𝑋, 𝑌})) → (𝑁‘{𝑋, 𝑌}) ∈ (LSubSp‘𝑈))
15		simpr 488	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝐸 ∈ (𝑁‘{𝑋, 𝑌})) → 𝐸 ∈ (𝑁‘{𝑋, 𝑌}))
16	10, 4, 12, 14, 15	lspsnel5a 19850	. . . . . . 7 ⊢ ((𝜑 ∧ 𝐸 ∈ (𝑁‘{𝑋, 𝑌})) → (𝑁‘{𝐸}) ⊆ (𝑁‘{𝑋, 𝑌}))
17	16	ssneld 3896	. . . . . 6 ⊢ ((𝜑 ∧ 𝐸 ∈ (𝑁‘{𝑋, 𝑌})) → (¬ 𝑧 ∈ (𝑁‘{𝑋, 𝑌}) → ¬ 𝑧 ∈ (𝑁‘{𝐸})))
18	17	ancld 554	. . . . 5 ⊢ ((𝜑 ∧ 𝐸 ∈ (𝑁‘{𝑋, 𝑌})) → (¬ 𝑧 ∈ (𝑁‘{𝑋, 𝑌}) → (¬ 𝑧 ∈ (𝑁‘{𝑋, 𝑌}) ∧ ¬ 𝑧 ∈ (𝑁‘{𝐸}))))
19	18	reximdv 3197	. . . 4 ⊢ ((𝜑 ∧ 𝐸 ∈ (𝑁‘{𝑋, 𝑌})) → (∃𝑧 ∈ 𝑉 ¬ 𝑧 ∈ (𝑁‘{𝑋, 𝑌}) → ∃𝑧 ∈ 𝑉 (¬ 𝑧 ∈ (𝑁‘{𝑋, 𝑌}) ∧ ¬ 𝑧 ∈ (𝑁‘{𝐸}))))
20	9, 19	mpd 15	. . 3 ⊢ ((𝜑 ∧ 𝐸 ∈ (𝑁‘{𝑋, 𝑌})) → ∃𝑧 ∈ 𝑉 (¬ 𝑧 ∈ (𝑁‘{𝑋, 𝑌}) ∧ ¬ 𝑧 ∈ (𝑁‘{𝐸})))
21		eqid 2758	. . . . . . . . . 10 ⊢ (Base‘𝐾) = (Base‘𝐾)
22		eqid 2758	. . . . . . . . . 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 38723	. . . . . . . . 9 ⊢ (𝜑 → 𝐸 ∈ (𝑉 ∖ { 0 }))
26	25	eldifad 3872	. . . . . . . 8 ⊢ (𝜑 → 𝐸 ∈ 𝑉)
27	1, 2, 3, 4, 5, 26, 7	dvh3dim 39057	. . . . . . 7 ⊢ (𝜑 → ∃𝑧 ∈ 𝑉 ¬ 𝑧 ∈ (𝑁‘{𝐸, 𝑌}))
28	27	adantr 484	. . . . . 6 ⊢ ((𝜑 ∧ 𝑋 = 0 ) → ∃𝑧 ∈ 𝑉 ¬ 𝑧 ∈ (𝑁‘{𝐸, 𝑌}))
29		preq1 4629	. . . . . . . . . . . . 13 ⊢ (𝑋 = 0 → {𝑋, 𝑌} = { 0 , 𝑌})
30		prcom 4628	. . . . . . . . . . . . 13 ⊢ { 0 , 𝑌} = {𝑌, 0 }
31	29, 30	eqtrdi 2809	. . . . . . . . . . . 12 ⊢ (𝑋 = 0 → {𝑋, 𝑌} = {𝑌, 0 })
32	31	fveq2d 6667	. . . . . . . . . . 11 ⊢ (𝑋 = 0 → (𝑁‘{𝑋, 𝑌}) = (𝑁‘{𝑌, 0 }))
33	3, 23, 4, 11, 7	lsppr0 19946	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑁‘{𝑌, 0 }) = (𝑁‘{𝑌}))
34	32, 33	sylan9eqr 2815	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑋 = 0 ) → (𝑁‘{𝑋, 𝑌}) = (𝑁‘{𝑌}))
35	3, 10, 4, 11, 26, 7	lspprcl 19832	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑁‘{𝐸, 𝑌}) ∈ (LSubSp‘𝑈))
36	3, 4, 11, 26, 7	lspprid2 19852	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑌 ∈ (𝑁‘{𝐸, 𝑌}))
37	10, 4, 11, 35, 36	lspsnel5a 19850	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑁‘{𝑌}) ⊆ (𝑁‘{𝐸, 𝑌}))
38	37	adantr 484	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑋 = 0 ) → (𝑁‘{𝑌}) ⊆ (𝑁‘{𝐸, 𝑌}))
39	34, 38	eqsstrd 3932	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑋 = 0 ) → (𝑁‘{𝑋, 𝑌}) ⊆ (𝑁‘{𝐸, 𝑌}))
40	39	ssneld 3896	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑋 = 0 ) → (¬ 𝑧 ∈ (𝑁‘{𝐸, 𝑌}) → ¬ 𝑧 ∈ (𝑁‘{𝑋, 𝑌})))
41	3, 4, 11, 26, 7	lspprid1 19851	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐸 ∈ (𝑁‘{𝐸, 𝑌}))
42	10, 4, 11, 35, 41	lspsnel5a 19850	. . . . . . . . . 10 ⊢ (𝜑 → (𝑁‘{𝐸}) ⊆ (𝑁‘{𝐸, 𝑌}))
43	42	adantr 484	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑋 = 0 ) → (𝑁‘{𝐸}) ⊆ (𝑁‘{𝐸, 𝑌}))
44	43	ssneld 3896	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑋 = 0 ) → (¬ 𝑧 ∈ (𝑁‘{𝐸, 𝑌}) → ¬ 𝑧 ∈ (𝑁‘{𝐸})))
45	40, 44	jcad 516	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑋 = 0 ) → (¬ 𝑧 ∈ (𝑁‘{𝐸, 𝑌}) → (¬ 𝑧 ∈ (𝑁‘{𝑋, 𝑌}) ∧ ¬ 𝑧 ∈ (𝑁‘{𝐸}))))
46	45	reximdv 3197	. . . . . 6 ⊢ ((𝜑 ∧ 𝑋 = 0 ) → (∃𝑧 ∈ 𝑉 ¬ 𝑧 ∈ (𝑁‘{𝐸, 𝑌}) → ∃𝑧 ∈ 𝑉 (¬ 𝑧 ∈ (𝑁‘{𝑋, 𝑌}) ∧ ¬ 𝑧 ∈ (𝑁‘{𝐸}))))
47	28, 46	mpd 15	. . . . 5 ⊢ ((𝜑 ∧ 𝑋 = 0 ) → ∃𝑧 ∈ 𝑉 (¬ 𝑧 ∈ (𝑁‘{𝑋, 𝑌}) ∧ ¬ 𝑧 ∈ (𝑁‘{𝐸})))
48	47	adantlr 714	. . . 4 ⊢ (((𝜑 ∧ ¬ 𝐸 ∈ (𝑁‘{𝑋, 𝑌})) ∧ 𝑋 = 0 ) → ∃𝑧 ∈ 𝑉 (¬ 𝑧 ∈ (𝑁‘{𝑋, 𝑌}) ∧ ¬ 𝑧 ∈ (𝑁‘{𝐸})))
49		hdmap11.p	. . . . . . . 8 ⊢ + = (+_g‘𝑈)
50	3, 49	lmodvacl 19730	. . . . . . 7 ⊢ ((𝑈 ∈ LMod ∧ 𝐸 ∈ 𝑉 ∧ 𝑋 ∈ 𝑉) → (𝐸 + 𝑋) ∈ 𝑉)
51	11, 26, 6, 50	syl3anc 1368	. . . . . 6 ⊢ (𝜑 → (𝐸 + 𝑋) ∈ 𝑉)
52	51	ad2antrr 725	. . . . 5 ⊢ (((𝜑 ∧ ¬ 𝐸 ∈ (𝑁‘{𝑋, 𝑌})) ∧ 𝑋 ≠ 0 ) → (𝐸 + 𝑋) ∈ 𝑉)
53	11	ad2antrr 725	. . . . . 6 ⊢ (((𝜑 ∧ ¬ 𝐸 ∈ (𝑁‘{𝑋, 𝑌})) ∧ 𝑋 ≠ 0 ) → 𝑈 ∈ LMod)
54	13	ad2antrr 725	. . . . . 6 ⊢ (((𝜑 ∧ ¬ 𝐸 ∈ (𝑁‘{𝑋, 𝑌})) ∧ 𝑋 ≠ 0 ) → (𝑁‘{𝑋, 𝑌}) ∈ (LSubSp‘𝑈))
55	3, 4, 11, 6, 7	lspprid1 19851	. . . . . . 7 ⊢ (𝜑 → 𝑋 ∈ (𝑁‘{𝑋, 𝑌}))
56	55	ad2antrr 725	. . . . . 6 ⊢ (((𝜑 ∧ ¬ 𝐸 ∈ (𝑁‘{𝑋, 𝑌})) ∧ 𝑋 ≠ 0 ) → 𝑋 ∈ (𝑁‘{𝑋, 𝑌}))
57	26	ad2antrr 725	. . . . . 6 ⊢ (((𝜑 ∧ ¬ 𝐸 ∈ (𝑁‘{𝑋, 𝑌})) ∧ 𝑋 ≠ 0 ) → 𝐸 ∈ 𝑉)
58		simplr 768	. . . . . 6 ⊢ (((𝜑 ∧ ¬ 𝐸 ∈ (𝑁‘{𝑋, 𝑌})) ∧ 𝑋 ≠ 0 ) → ¬ 𝐸 ∈ (𝑁‘{𝑋, 𝑌}))
59	3, 49, 10, 53, 54, 56, 57, 58	lssvancl2 19799	. . . . 5 ⊢ (((𝜑 ∧ ¬ 𝐸 ∈ (𝑁‘{𝑋, 𝑌})) ∧ 𝑋 ≠ 0 ) → ¬ (𝐸 + 𝑋) ∈ (𝑁‘{𝑋, 𝑌}))
60	3, 10, 4	lspsncl 19831	. . . . . . . 8 ⊢ ((𝑈 ∈ LMod ∧ 𝐸 ∈ 𝑉) → (𝑁‘{𝐸}) ∈ (LSubSp‘𝑈))
61	11, 26, 60	syl2anc 587	. . . . . . 7 ⊢ (𝜑 → (𝑁‘{𝐸}) ∈ (LSubSp‘𝑈))
62	61	ad2antrr 725	. . . . . 6 ⊢ (((𝜑 ∧ ¬ 𝐸 ∈ (𝑁‘{𝑋, 𝑌})) ∧ 𝑋 ≠ 0 ) → (𝑁‘{𝐸}) ∈ (LSubSp‘𝑈))
63	3, 4	lspsnid 19847	. . . . . . . 8 ⊢ ((𝑈 ∈ LMod ∧ 𝐸 ∈ 𝑉) → 𝐸 ∈ (𝑁‘{𝐸}))
64	11, 26, 63	syl2anc 587	. . . . . . 7 ⊢ (𝜑 → 𝐸 ∈ (𝑁‘{𝐸}))
65	64	ad2antrr 725	. . . . . 6 ⊢ (((𝜑 ∧ ¬ 𝐸 ∈ (𝑁‘{𝑋, 𝑌})) ∧ 𝑋 ≠ 0 ) → 𝐸 ∈ (𝑁‘{𝐸}))
66	6	ad2antrr 725	. . . . . 6 ⊢ (((𝜑 ∧ ¬ 𝐸 ∈ (𝑁‘{𝑋, 𝑌})) ∧ 𝑋 ≠ 0 ) → 𝑋 ∈ 𝑉)
67	1, 2, 5	dvhlvec 38720	. . . . . . . 8 ⊢ (𝜑 → 𝑈 ∈ LVec)
68	67	ad2antrr 725	. . . . . . 7 ⊢ (((𝜑 ∧ ¬ 𝐸 ∈ (𝑁‘{𝑋, 𝑌})) ∧ 𝑋 ≠ 0 ) → 𝑈 ∈ LVec)
69		simpr 488	. . . . . . . 8 ⊢ (((𝜑 ∧ ¬ 𝐸 ∈ (𝑁‘{𝑋, 𝑌})) ∧ 𝑋 ≠ 0 ) → 𝑋 ≠ 0 )
70		eldifsn 4680	. . . . . . . 8 ⊢ (𝑋 ∈ (𝑉 ∖ { 0 }) ↔ (𝑋 ∈ 𝑉 ∧ 𝑋 ≠ 0 ))
71	66, 69, 70	sylanbrc 586	. . . . . . 7 ⊢ (((𝜑 ∧ ¬ 𝐸 ∈ (𝑁‘{𝑋, 𝑌})) ∧ 𝑋 ≠ 0 ) → 𝑋 ∈ (𝑉 ∖ { 0 }))
72	10, 4, 11, 13, 55	lspsnel5a 19850	. . . . . . . . . 10 ⊢ (𝜑 → (𝑁‘{𝑋}) ⊆ (𝑁‘{𝑋, 𝑌}))
73	72	sseld 3893	. . . . . . . . 9 ⊢ (𝜑 → (𝐸 ∈ (𝑁‘{𝑋}) → 𝐸 ∈ (𝑁‘{𝑋, 𝑌})))
74	73	con3dimp 412	. . . . . . . 8 ⊢ ((𝜑 ∧ ¬ 𝐸 ∈ (𝑁‘{𝑋, 𝑌})) → ¬ 𝐸 ∈ (𝑁‘{𝑋}))
75	74	adantr 484	. . . . . . 7 ⊢ (((𝜑 ∧ ¬ 𝐸 ∈ (𝑁‘{𝑋, 𝑌})) ∧ 𝑋 ≠ 0 ) → ¬ 𝐸 ∈ (𝑁‘{𝑋}))
76	3, 23, 4, 68, 57, 71, 75	lspsnnecom 19973	. . . . . 6 ⊢ (((𝜑 ∧ ¬ 𝐸 ∈ (𝑁‘{𝑋, 𝑌})) ∧ 𝑋 ≠ 0 ) → ¬ 𝑋 ∈ (𝑁‘{𝐸}))
77	3, 49, 10, 53, 62, 65, 66, 76	lssvancl1 19798	. . . . 5 ⊢ (((𝜑 ∧ ¬ 𝐸 ∈ (𝑁‘{𝑋, 𝑌})) ∧ 𝑋 ≠ 0 ) → ¬ (𝐸 + 𝑋) ∈ (𝑁‘{𝐸}))
78		eleq1 2839	. . . . . . . 8 ⊢ (𝑧 = (𝐸 + 𝑋) → (𝑧 ∈ (𝑁‘{𝑋, 𝑌}) ↔ (𝐸 + 𝑋) ∈ (𝑁‘{𝑋, 𝑌})))
79	78	notbid 321	. . . . . . 7 ⊢ (𝑧 = (𝐸 + 𝑋) → (¬ 𝑧 ∈ (𝑁‘{𝑋, 𝑌}) ↔ ¬ (𝐸 + 𝑋) ∈ (𝑁‘{𝑋, 𝑌})))
80		eleq1 2839	. . . . . . . 8 ⊢ (𝑧 = (𝐸 + 𝑋) → (𝑧 ∈ (𝑁‘{𝐸}) ↔ (𝐸 + 𝑋) ∈ (𝑁‘{𝐸})))
81	80	notbid 321	. . . . . . 7 ⊢ (𝑧 = (𝐸 + 𝑋) → (¬ 𝑧 ∈ (𝑁‘{𝐸}) ↔ ¬ (𝐸 + 𝑋) ∈ (𝑁‘{𝐸})))
82	79, 81	anbi12d 633	. . . . . 6 ⊢ (𝑧 = (𝐸 + 𝑋) → ((¬ 𝑧 ∈ (𝑁‘{𝑋, 𝑌}) ∧ ¬ 𝑧 ∈ (𝑁‘{𝐸})) ↔ (¬ (𝐸 + 𝑋) ∈ (𝑁‘{𝑋, 𝑌}) ∧ ¬ (𝐸 + 𝑋) ∈ (𝑁‘{𝐸}))))
83	82	rspcev 3543	. . . . 5 ⊢ (((𝐸 + 𝑋) ∈ 𝑉 ∧ (¬ (𝐸 + 𝑋) ∈ (𝑁‘{𝑋, 𝑌}) ∧ ¬ (𝐸 + 𝑋) ∈ (𝑁‘{𝐸}))) → ∃𝑧 ∈ 𝑉 (¬ 𝑧 ∈ (𝑁‘{𝑋, 𝑌}) ∧ ¬ 𝑧 ∈ (𝑁‘{𝐸})))
84	52, 59, 77, 83	syl12anc 835	. . . 4 ⊢ (((𝜑 ∧ ¬ 𝐸 ∈ (𝑁‘{𝑋, 𝑌})) ∧ 𝑋 ≠ 0 ) → ∃𝑧 ∈ 𝑉 (¬ 𝑧 ∈ (𝑁‘{𝑋, 𝑌}) ∧ ¬ 𝑧 ∈ (𝑁‘{𝐸})))
85	48, 84	pm2.61dane 3038	. . 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 1130	. . . 4 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑉 ∧ (¬ 𝑧 ∈ (𝑁‘{𝑋, 𝑌}) ∧ ¬ 𝑧 ∈ (𝑁‘{𝐸}))) → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))
91	6	3ad2ant1 1130	. . . 4 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑉 ∧ (¬ 𝑧 ∈ (𝑁‘{𝑋, 𝑌}) ∧ ¬ 𝑧 ∈ (𝑁‘{𝐸}))) → 𝑋 ∈ 𝑉)
92	7	3ad2ant1 1130	. . . 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 1134	. . . 4 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑉 ∧ (¬ 𝑧 ∈ (𝑁‘{𝑋, 𝑌}) ∧ ¬ 𝑧 ∈ (𝑁‘{𝐸}))) → 𝑧 ∈ 𝑉)
99		simp3l 1198	. . . 4 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑉 ∧ (¬ 𝑧 ∈ (𝑁‘{𝑋, 𝑌}) ∧ ¬ 𝑧 ∈ (𝑁‘{𝐸}))) → ¬ 𝑧 ∈ (𝑁‘{𝑋, 𝑌}))
100	11	3ad2ant1 1130	. . . . 5 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑉 ∧ (¬ 𝑧 ∈ (𝑁‘{𝑋, 𝑌}) ∧ ¬ 𝑧 ∈ (𝑁‘{𝐸}))) → 𝑈 ∈ LMod)
101	26	3ad2ant1 1130	. . . . 5 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑉 ∧ (¬ 𝑧 ∈ (𝑁‘{𝑋, 𝑌}) ∧ ¬ 𝑧 ∈ (𝑁‘{𝐸}))) → 𝐸 ∈ 𝑉)
102		simp3r 1199	. . . . 5 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑉 ∧ (¬ 𝑧 ∈ (𝑁‘{𝑋, 𝑌}) ∧ ¬ 𝑧 ∈ (𝑁‘{𝐸}))) → ¬ 𝑧 ∈ (𝑁‘{𝐸}))
103	3, 4, 100, 98, 101, 102	lspsnne2 19972	. . . 4 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑉 ∧ (¬ 𝑧 ∈ (𝑁‘{𝑋, 𝑌}) ∧ ¬ 𝑧 ∈ (𝑁‘{𝐸}))) → (𝑁‘{𝑧}) ≠ (𝑁‘{𝐸}))
104	1, 2, 3, 49, 87, 88, 89, 90, 91, 92, 24, 23, 4, 93, 94, 95, 96, 97, 98, 99, 103	hdmap11lem1 39452	. . 3 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑉 ∧ (¬ 𝑧 ∈ (𝑁‘{𝑋, 𝑌}) ∧ ¬ 𝑧 ∈ (𝑁‘{𝐸}))) → (𝑆‘(𝑋 + 𝑌)) = ((𝑆‘𝑋) ✚ (𝑆‘𝑌)))
105	104	rexlimdv3a 3210	. 2 ⊢ (𝜑 → (∃𝑧 ∈ 𝑉 (¬ 𝑧 ∈ (𝑁‘{𝑋, 𝑌}) ∧ ¬ 𝑧 ∈ (𝑁‘{𝐸})) → (𝑆‘(𝑋 + 𝑌)) = ((𝑆‘𝑋) ✚ (𝑆‘𝑌))))
106	86, 105	mpd 15	1 ⊢ (𝜑 → (𝑆‘(𝑋 + 𝑌)) = ((𝑆‘𝑋) ✚ (𝑆‘𝑌)))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ∧ wa 399 ∧ w3a 1084 = wceq 1538 ∈ wcel 2111 ≠ wne 2951 ∃wrex 3071 ∖ cdif 3857 ⊆ wss 3860 {csn 4525 {cpr 4527 ⟨cop 4531 I cid 5433 ↾ cres 5530 ‘cfv 6340 (class class class)co 7156 Basecbs 16555 +_gcplusg 16637 0_gc0g 16785 LModclmod 19716 LSubSpclss 19785 LSpanclspn 19825 LVecclvec 19956 HLchlt 36961 LHypclh 37595 LTrncltrn 37712 DVecHcdvh 38689 LCDualclcd 39197 mapdcmpd 39235 HVMapchvm 39367 HDMap1chdma1 39402 HDMapchdma 39403

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1911 ax-6 1970 ax-7 2015 ax-8 2113 ax-9 2121 ax-10 2142 ax-11 2158 ax-12 2175 ax-ext 2729 ax-rep 5160 ax-sep 5173 ax-nul 5180 ax-pow 5238 ax-pr 5302 ax-un 7465 ax-cnex 10644 ax-resscn 10645 ax-1cn 10646 ax-icn 10647 ax-addcl 10648 ax-addrcl 10649 ax-mulcl 10650 ax-mulrcl 10651 ax-mulcom 10652 ax-addass 10653 ax-mulass 10654 ax-distr 10655 ax-i2m1 10656 ax-1ne0 10657 ax-1rid 10658 ax-rnegex 10659 ax-rrecex 10660 ax-cnre 10661 ax-pre-lttri 10662 ax-pre-lttrn 10663 ax-pre-ltadd 10664 ax-pre-mulgt0 10665 ax-riotaBAD 36564

This theorem depends on definitions: df-bi 210 df-an 400 df-or 845 df-3or 1085 df-3an 1086 df-tru 1541 df-fal 1551 df-ex 1782 df-nf 1786 df-sb 2070 df-mo 2557 df-eu 2588 df-clab 2736 df-cleq 2750 df-clel 2830 df-nfc 2901 df-ne 2952 df-nel 3056 df-ral 3075 df-rex 3076 df-reu 3077 df-rmo 3078 df-rab 3079 df-v 3411 df-sbc 3699 df-csb 3808 df-dif 3863 df-un 3865 df-in 3867 df-ss 3877 df-pss 3879 df-nul 4228 df-if 4424 df-pw 4499 df-sn 4526 df-pr 4528 df-tp 4530 df-op 4532 df-ot 4534 df-uni 4802 df-int 4842 df-iun 4888 df-iin 4889 df-br 5037 df-opab 5099 df-mpt 5117 df-tr 5143 df-id 5434 df-eprel 5439 df-po 5447 df-so 5448 df-fr 5487 df-we 5489 df-xp 5534 df-rel 5535 df-cnv 5536 df-co 5537 df-dm 5538 df-rn 5539 df-res 5540 df-ima 5541 df-pred 6131 df-ord 6177 df-on 6178 df-lim 6179 df-suc 6180 df-iota 6299 df-fun 6342 df-fn 6343 df-f 6344 df-f1 6345 df-fo 6346 df-f1o 6347 df-fv 6348 df-riota 7114 df-ov 7159 df-oprab 7160 df-mpo 7161 df-of 7411 df-om 7586 df-1st 7699 df-2nd 7700 df-tpos 7908 df-undef 7955 df-wrecs 7963 df-recs 8024 df-rdg 8062 df-1o 8118 df-er 8305 df-map 8424 df-en 8541 df-dom 8542 df-sdom 8543 df-fin 8544 df-pnf 10728 df-mnf 10729 df-xr 10730 df-ltxr 10731 df-le 10732 df-sub 10923 df-neg 10924 df-nn 11688 df-2 11750 df-3 11751 df-4 11752 df-5 11753 df-6 11754 df-n0 11948 df-z 12034 df-uz 12296 df-fz 12953 df-struct 16557 df-ndx 16558 df-slot 16559 df-base 16561 df-sets 16562 df-ress 16563 df-plusg 16650 df-mulr 16651 df-sca 16653 df-vsca 16654 df-0g 16787 df-mre 16929 df-mrc 16930 df-acs 16932 df-proset 17618 df-poset 17636 df-plt 17648 df-lub 17664 df-glb 17665 df-join 17666 df-meet 17667 df-p0 17729 df-p1 17730 df-lat 17736 df-clat 17798 df-mgm 17932 df-sgrp 17981 df-mnd 17992 df-submnd 18037 df-grp 18186 df-minusg 18187 df-sbg 18188 df-subg 18357 df-cntz 18528 df-oppg 18555 df-lsm 18842 df-cmn 18989 df-abl 18990 df-mgp 19322 df-ur 19334 df-ring 19381 df-oppr 19458 df-dvdsr 19476 df-unit 19477 df-invr 19507 df-dvr 19518 df-drng 19586 df-lmod 19718 df-lss 19786 df-lsp 19826 df-lvec 19957 df-lsatoms 36587 df-lshyp 36588 df-lcv 36630 df-lfl 36669 df-lkr 36697 df-ldual 36735 df-oposet 36787 df-ol 36789 df-oml 36790 df-covers 36877 df-ats 36878 df-atl 36909 df-cvlat 36933 df-hlat 36962 df-llines 37109 df-lplanes 37110 df-lvols 37111 df-lines 37112 df-psubsp 37114 df-pmap 37115 df-padd 37407 df-lhyp 37599 df-laut 37600 df-ldil 37715 df-ltrn 37716 df-trl 37770 df-tgrp 38354 df-tendo 38366 df-edring 38368 df-dveca 38614 df-disoa 38640 df-dvech 38690 df-dib 38750 df-dic 38784 df-dih 38840 df-doch 38959 df-djh 39006 df-lcdual 39198 df-mapd 39236 df-hvmap 39368 df-hdmap1 39404 df-hdmap 39405

This theorem is referenced by: hdmapadd 39454

W3C validator