Metamath Proof Explorer


Theorem mapdh6bN

Description: Lemmma for mapdh6N . (Contributed by NM, 24-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
mapdh6b.y φ Y = 0 ˙
mapdh6b.z φ Z V
mapdh6b.ne φ ¬ X N Y Z
Assertion mapdh6bN φ I X F Y + ˙ Z = I X F Y ˙ I X F 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 mapdh6b.y φ Y = 0 ˙
21 mapdh6b.z φ Z V
22 mapdh6b.ne φ ¬ X N Y Z
23 3 10 14 lcdlmod φ C LMod
24 lmodgrp C LMod C Grp
25 23 24 syl φ C Grp
26 3 5 14 dvhlvec φ U LVec
27 17 eldifad φ X V
28 3 5 14 dvhlmod φ U LMod
29 6 8 lmod0vcl U LMod 0 ˙ V
30 28 29 syl φ 0 ˙ V
31 20 30 eqeltrd φ Y V
32 6 9 26 27 31 21 22 lspindpi φ N X N Y N X N Z
33 32 simprd φ N X N Z
34 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 21 33 mapdhcl φ I X F Z D
35 11 19 1 grplid C Grp I X F Z D Q ˙ I X F Z = I X F Z
36 25 34 35 syl2anc φ Q ˙ I X F Z = I X F Z
37 20 oteq3d φ X F Y = X F 0 ˙
38 37 fveq2d φ I X F Y = I X F 0 ˙
39 1 2 8 17 15 mapdhval0 φ I X F 0 ˙ = Q
40 38 39 eqtrd φ I X F Y = Q
41 40 oveq1d φ I X F Y ˙ I X F Z = Q ˙ I X F Z
42 20 oveq1d φ Y + ˙ Z = 0 ˙ + ˙ Z
43 lmodgrp U LMod U Grp
44 28 43 syl φ U Grp
45 6 18 8 grplid U Grp Z V 0 ˙ + ˙ Z = Z
46 44 21 45 syl2anc φ 0 ˙ + ˙ Z = Z
47 42 46 eqtrd φ Y + ˙ Z = Z
48 47 oteq3d φ X F Y + ˙ Z = X F Z
49 48 fveq2d φ I X F Y + ˙ Z = I X F Z
50 36 41 49 3eqtr4rd φ I X F Y + ˙ Z = I X F Y ˙ I X F Z