Metamath Proof Explorer


Theorem mapdh8g

Description: Part of Part (8) in Baer p. 48. Eliminate X e. ( N{ Y , T } ) . TODO: break out T =/= .0. in mapdh8e so we can share hypotheses. Also, look at hypothesis sharing for earlier mapdh8* and mapdh75* stuff. (Contributed by NM, 10-May-2015)

Ref Expression
Hypotheses mapdh8a.h H = LHyp K
mapdh8a.u U = DVecH K W
mapdh8a.v V = Base U
mapdh8a.s - ˙ = - U
mapdh8a.o 0 ˙ = 0 U
mapdh8a.n N = LSpan U
mapdh8a.c C = LCDual K W
mapdh8a.d D = Base C
mapdh8a.r R = - C
mapdh8a.q Q = 0 C
mapdh8a.j J = LSpan C
mapdh8a.m M = mapd K W
mapdh8a.i I = x V if 2 nd x = 0 ˙ Q ι h D | M N 2 nd x = J h M N 1 st 1 st x - ˙ 2 nd x = J 2 nd 1 st x R h
mapdh8a.k φ K HL W H
mapdh8e.f φ F D
mapdh8e.mn φ M N X = J F
mapdh8e.eg φ I X F Y = G
mapdh8e.x φ X V 0 ˙
mapdh8e.y φ Y V 0 ˙
mapdh8e.t φ T V 0 ˙
mapdh8e.xy φ N X N Y
mapdh8e.xt φ N X N T
mapdh8e.yt φ N Y N T
Assertion mapdh8g φ I Y G T = I X F T

Proof

Step Hyp Ref Expression
1 mapdh8a.h H = LHyp K
2 mapdh8a.u U = DVecH K W
3 mapdh8a.v V = Base U
4 mapdh8a.s - ˙ = - U
5 mapdh8a.o 0 ˙ = 0 U
6 mapdh8a.n N = LSpan U
7 mapdh8a.c C = LCDual K W
8 mapdh8a.d D = Base C
9 mapdh8a.r R = - C
10 mapdh8a.q Q = 0 C
11 mapdh8a.j J = LSpan C
12 mapdh8a.m M = mapd K W
13 mapdh8a.i I = x V if 2 nd x = 0 ˙ Q ι h D | M N 2 nd x = J h M N 1 st 1 st x - ˙ 2 nd x = J 2 nd 1 st x R h
14 mapdh8a.k φ K HL W H
15 mapdh8e.f φ F D
16 mapdh8e.mn φ M N X = J F
17 mapdh8e.eg φ I X F Y = G
18 mapdh8e.x φ X V 0 ˙
19 mapdh8e.y φ Y V 0 ˙
20 mapdh8e.t φ T V 0 ˙
21 mapdh8e.xy φ N X N Y
22 mapdh8e.xt φ N X N T
23 mapdh8e.yt φ N Y N T
24 14 adantr φ X N Y T K HL W H
25 15 adantr φ X N Y T F D
26 16 adantr φ X N Y T M N X = J F
27 17 adantr φ X N Y T I X F Y = G
28 18 adantr φ X N Y T X V 0 ˙
29 19 adantr φ X N Y T Y V 0 ˙
30 20 adantr φ X N Y T T V 0 ˙
31 21 adantr φ X N Y T N X N Y
32 22 adantr φ X N Y T N X N T
33 23 adantr φ X N Y T N Y N T
34 simpr φ X N Y T X N Y T
35 1 2 3 4 5 6 7 8 9 10 11 12 13 24 25 26 27 28 29 30 31 32 33 34 mapdh8e φ X N Y T I Y G T = I X F T
36 14 adantr φ ¬ X N Y T K HL W H
37 15 adantr φ ¬ X N Y T F D
38 16 adantr φ ¬ X N Y T M N X = J F
39 17 adantr φ ¬ X N Y T I X F Y = G
40 18 adantr φ ¬ X N Y T X V 0 ˙
41 19 adantr φ ¬ X N Y T Y V 0 ˙
42 23 adantr φ ¬ X N Y T N Y N T
43 20 adantr φ ¬ X N Y T T V 0 ˙
44 simpr φ ¬ X N Y T ¬ X N Y T
45 1 2 3 4 5 6 7 8 9 10 11 12 13 36 37 38 39 40 41 42 43 44 mapdh8a φ ¬ X N Y T I Y G T = I X F T
46 35 45 pm2.61dan φ I Y G T = I X F T