Metamath Proof Explorer


Theorem hdmap1l6j

Description: Lemmma for hdmap1l6 . Eliminate ( N { Y } ) = ( N { Z } ) hypothesis. (Contributed by NM, 1-May-2015)

Ref Expression
Hypotheses hdmap1l6.h H = LHyp K
hdmap1l6.u U = DVecH K W
hdmap1l6.v V = Base U
hdmap1l6.p + ˙ = + U
hdmap1l6.s - ˙ = - U
hdmap1l6c.o 0 ˙ = 0 U
hdmap1l6.n N = LSpan U
hdmap1l6.c C = LCDual K W
hdmap1l6.d D = Base C
hdmap1l6.a ˙ = + C
hdmap1l6.r R = - C
hdmap1l6.q Q = 0 C
hdmap1l6.l L = LSpan C
hdmap1l6.m M = mapd K W
hdmap1l6.i I = HDMap1 K W
hdmap1l6.k φ K HL W H
hdmap1l6.f φ F D
hdmap1l6cl.x φ X V 0 ˙
hdmap1l6.mn φ M N X = L F
hdmap1l6i.xn φ ¬ X N Y Z
hdmap1l6i.y φ Y V 0 ˙
hdmap1l6i.z φ Z V 0 ˙
Assertion hdmap1l6j φ I X F Y + ˙ Z = I X F Y ˙ I X F Z

Proof

Step Hyp Ref Expression
1 hdmap1l6.h H = LHyp K
2 hdmap1l6.u U = DVecH K W
3 hdmap1l6.v V = Base U
4 hdmap1l6.p + ˙ = + U
5 hdmap1l6.s - ˙ = - U
6 hdmap1l6c.o 0 ˙ = 0 U
7 hdmap1l6.n N = LSpan U
8 hdmap1l6.c C = LCDual K W
9 hdmap1l6.d D = Base C
10 hdmap1l6.a ˙ = + C
11 hdmap1l6.r R = - C
12 hdmap1l6.q Q = 0 C
13 hdmap1l6.l L = LSpan C
14 hdmap1l6.m M = mapd K W
15 hdmap1l6.i I = HDMap1 K W
16 hdmap1l6.k φ K HL W H
17 hdmap1l6.f φ F D
18 hdmap1l6cl.x φ X V 0 ˙
19 hdmap1l6.mn φ M N X = L F
20 hdmap1l6i.xn φ ¬ X N Y Z
21 hdmap1l6i.y φ Y V 0 ˙
22 hdmap1l6i.z φ Z V 0 ˙
23 16 adantr φ N Y = N Z K HL W H
24 17 adantr φ N Y = N Z F D
25 18 adantr φ N Y = N Z X V 0 ˙
26 19 adantr φ N Y = N Z M N X = L F
27 20 adantr φ N Y = N Z ¬ X N Y Z
28 21 adantr φ N Y = N Z Y V 0 ˙
29 22 adantr φ N Y = N Z Z V 0 ˙
30 simpr φ N Y = N Z N Y = N Z
31 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 23 24 25 26 27 28 29 30 hdmap1l6i φ N Y = N Z I X F Y + ˙ Z = I X F Y ˙ I X F Z
32 16 adantr φ N Y N Z K HL W H
33 17 adantr φ N Y N Z F D
34 18 adantr φ N Y N Z X V 0 ˙
35 19 adantr φ N Y N Z M N X = L F
36 21 adantr φ N Y N Z Y V 0 ˙
37 22 adantr φ N Y N Z Z V 0 ˙
38 20 adantr φ N Y N Z ¬ X N Y Z
39 simpr φ N Y N Z N Y N Z
40 eqidd φ N Y N Z I X F Y = I X F Y
41 eqidd φ N Y N Z I X F Z = I X F Z
42 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 32 33 34 35 36 37 38 39 40 41 hdmap1l6a φ N Y N Z I X F Y + ˙ Z = I X F Y ˙ I X F Z
43 31 42 pm2.61dane φ I X F Y + ˙ Z = I X F Y ˙ I X F Z