Metamath Proof Explorer


Theorem hdmap14lem10

Description: Part of proof of part 14 in Baer p. 49 line 38. (Contributed by NM, 3-Jun-2015)

Ref Expression
Hypotheses hdmap14lem8.h H=LHypK
hdmap14lem8.u U=DVecHKW
hdmap14lem8.v V=BaseU
hdmap14lem8.q +˙=+U
hdmap14lem8.t ·˙=U
hdmap14lem8.o 0˙=0U
hdmap14lem8.n N=LSpanU
hdmap14lem8.r R=ScalarU
hdmap14lem8.b B=BaseR
hdmap14lem8.c C=LCDualKW
hdmap14lem8.d ˙=+C
hdmap14lem8.e ˙=C
hdmap14lem8.p P=ScalarC
hdmap14lem8.a A=BaseP
hdmap14lem8.s S=HDMapKW
hdmap14lem8.k φKHLWH
hdmap14lem8.x φXV0˙
hdmap14lem8.y φYV0˙
hdmap14lem8.f φFB
hdmap14lem8.g φGA
hdmap14lem8.i φIA
hdmap14lem8.xx φSF·˙X=G˙SX
hdmap14lem8.yy φSF·˙Y=I˙SY
hdmap14lem8.ne φNXNY
Assertion hdmap14lem10 φG=I

Proof

Step Hyp Ref Expression
1 hdmap14lem8.h H=LHypK
2 hdmap14lem8.u U=DVecHKW
3 hdmap14lem8.v V=BaseU
4 hdmap14lem8.q +˙=+U
5 hdmap14lem8.t ·˙=U
6 hdmap14lem8.o 0˙=0U
7 hdmap14lem8.n N=LSpanU
8 hdmap14lem8.r R=ScalarU
9 hdmap14lem8.b B=BaseR
10 hdmap14lem8.c C=LCDualKW
11 hdmap14lem8.d ˙=+C
12 hdmap14lem8.e ˙=C
13 hdmap14lem8.p P=ScalarC
14 hdmap14lem8.a A=BaseP
15 hdmap14lem8.s S=HDMapKW
16 hdmap14lem8.k φKHLWH
17 hdmap14lem8.x φXV0˙
18 hdmap14lem8.y φYV0˙
19 hdmap14lem8.f φFB
20 hdmap14lem8.g φGA
21 hdmap14lem8.i φIA
22 hdmap14lem8.xx φSF·˙X=G˙SX
23 hdmap14lem8.yy φSF·˙Y=I˙SY
24 hdmap14lem8.ne φNXNY
25 eqid LSpanC=LSpanC
26 1 2 16 dvhlmod φULMod
27 17 eldifad φXV
28 18 eldifad φYV
29 3 4 lmodvacl ULModXVYVX+˙YV
30 26 27 28 29 syl3anc φX+˙YV
31 1 2 3 5 8 9 10 12 25 13 14 15 16 30 19 hdmap14lem2a φgASF·˙X+˙Y=g˙SX+˙Y
32 16 3ad2ant1 φgASF·˙X+˙Y=g˙SX+˙YKHLWH
33 17 3ad2ant1 φgASF·˙X+˙Y=g˙SX+˙YXV0˙
34 18 3ad2ant1 φgASF·˙X+˙Y=g˙SX+˙YYV0˙
35 19 3ad2ant1 φgASF·˙X+˙Y=g˙SX+˙YFB
36 20 3ad2ant1 φgASF·˙X+˙Y=g˙SX+˙YGA
37 21 3ad2ant1 φgASF·˙X+˙Y=g˙SX+˙YIA
38 22 3ad2ant1 φgASF·˙X+˙Y=g˙SX+˙YSF·˙X=G˙SX
39 23 3ad2ant1 φgASF·˙X+˙Y=g˙SX+˙YSF·˙Y=I˙SY
40 24 3ad2ant1 φgASF·˙X+˙Y=g˙SX+˙YNXNY
41 simp2 φgASF·˙X+˙Y=g˙SX+˙YgA
42 simp3 φgASF·˙X+˙Y=g˙SX+˙YSF·˙X+˙Y=g˙SX+˙Y
43 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 42 hdmap14lem9 φgASF·˙X+˙Y=g˙SX+˙YG=I
44 43 rexlimdv3a φgASF·˙X+˙Y=g˙SX+˙YG=I
45 31 44 mpd φG=I