Metamath Proof Explorer


Theorem mapdh6b0N

Description: Lemmma for mapdh6N . (Contributed by NM, 23-Apr-2015) (New usage is discouraged.)

Ref Expression
Hypotheses mapdh.q Q = 0 C
mapdh.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
mapdh.h H = LHyp K
mapdh.m M = mapd K W
mapdh.u U = DVecH K W
mapdh.v V = Base U
mapdh.s - ˙ = - U
mapdhc.o 0 ˙ = 0 U
mapdh.n N = LSpan U
mapdh.c C = LCDual K W
mapdh.d D = Base C
mapdh.r R = - C
mapdh.j J = LSpan C
mapdh.k φ K HL W H
mapdhc.f φ F D
mapdh.mn φ M N X = J F
mapdhcl.x φ X V 0 ˙
mapdh.p + ˙ = + U
mapdh.a ˙ = + C
mapdh6b0.y φ Y V
mapdh6b0.z φ Z V
mapdh6b0.ne φ N X N Y Z = 0 ˙
Assertion mapdh6b0N φ ¬ X N Y Z

Proof

Step Hyp Ref Expression
1 mapdh.q Q = 0 C
2 mapdh.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
3 mapdh.h H = LHyp K
4 mapdh.m M = mapd K W
5 mapdh.u U = DVecH K W
6 mapdh.v V = Base U
7 mapdh.s - ˙ = - U
8 mapdhc.o 0 ˙ = 0 U
9 mapdh.n N = LSpan U
10 mapdh.c C = LCDual K W
11 mapdh.d D = Base C
12 mapdh.r R = - C
13 mapdh.j J = LSpan C
14 mapdh.k φ K HL W H
15 mapdhc.f φ F D
16 mapdh.mn φ M N X = J F
17 mapdhcl.x φ X V 0 ˙
18 mapdh.p + ˙ = + U
19 mapdh.a ˙ = + C
20 mapdh6b0.y φ Y V
21 mapdh6b0.z φ Z V
22 mapdh6b0.ne φ N X N Y Z = 0 ˙
23 eqid LSubSp U = LSubSp U
24 3 5 14 dvhlvec φ U LVec
25 3 5 14 dvhlmod φ U LMod
26 6 23 9 25 20 21 lspprcl φ N Y Z LSubSp U
27 6 8 9 23 24 26 17 lspdisjb φ ¬ X N Y Z N X N Y Z = 0 ˙
28 22 27 mpbird φ ¬ X N Y Z