# Metamath Proof Explorer

## Theorem mapdpg

Description: Part 1 of proof of the first fundamental theorem of projective geometry. Part (1) in Baer p. 44. Our notation corresponds to Baer's as follows: M for *, N{ } for F(), J{ } for G(), X for x, G for x', Y for y, h for y'. TODO: Rename variables per mapdhval . (Contributed by NM, 22-Mar-2015)

Ref Expression
Hypotheses mapdpg.h ${⊢}{H}=\mathrm{LHyp}\left({K}\right)$
mapdpg.m ${⊢}{M}=\mathrm{mapd}\left({K}\right)\left({W}\right)$
mapdpg.u ${⊢}{U}=\mathrm{DVecH}\left({K}\right)\left({W}\right)$
mapdpg.v ${⊢}{V}={\mathrm{Base}}_{{U}}$
mapdpg.s
mapdpg.z
mapdpg.n ${⊢}{N}=\mathrm{LSpan}\left({U}\right)$
mapdpg.c ${⊢}{C}=\mathrm{LCDual}\left({K}\right)\left({W}\right)$
mapdpg.f ${⊢}{F}={\mathrm{Base}}_{{C}}$
mapdpg.r ${⊢}{R}={-}_{{C}}$
mapdpg.j ${⊢}{J}=\mathrm{LSpan}\left({C}\right)$
mapdpg.k ${⊢}{\phi }\to \left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)$
mapdpg.x
mapdpg.y
mapdpg.g ${⊢}{\phi }\to {G}\in {F}$
mapdpg.ne ${⊢}{\phi }\to {N}\left(\left\{{X}\right\}\right)\ne {N}\left(\left\{{Y}\right\}\right)$
mapdpg.e ${⊢}{\phi }\to {M}\left({N}\left(\left\{{X}\right\}\right)\right)={J}\left(\left\{{G}\right\}\right)$
Assertion mapdpg

### Proof

Step Hyp Ref Expression
1 mapdpg.h ${⊢}{H}=\mathrm{LHyp}\left({K}\right)$
2 mapdpg.m ${⊢}{M}=\mathrm{mapd}\left({K}\right)\left({W}\right)$
3 mapdpg.u ${⊢}{U}=\mathrm{DVecH}\left({K}\right)\left({W}\right)$
4 mapdpg.v ${⊢}{V}={\mathrm{Base}}_{{U}}$
5 mapdpg.s
6 mapdpg.z
7 mapdpg.n ${⊢}{N}=\mathrm{LSpan}\left({U}\right)$
8 mapdpg.c ${⊢}{C}=\mathrm{LCDual}\left({K}\right)\left({W}\right)$
9 mapdpg.f ${⊢}{F}={\mathrm{Base}}_{{C}}$
10 mapdpg.r ${⊢}{R}={-}_{{C}}$
11 mapdpg.j ${⊢}{J}=\mathrm{LSpan}\left({C}\right)$
12 mapdpg.k ${⊢}{\phi }\to \left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)$
13 mapdpg.x
14 mapdpg.y
15 mapdpg.g ${⊢}{\phi }\to {G}\in {F}$
16 mapdpg.ne ${⊢}{\phi }\to {N}\left(\left\{{X}\right\}\right)\ne {N}\left(\left\{{Y}\right\}\right)$
17 mapdpg.e ${⊢}{\phi }\to {M}\left({N}\left(\left\{{X}\right\}\right)\right)={J}\left(\left\{{G}\right\}\right)$
18 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 mapdpglem24
19 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 mapdpglem32
20 19 3exp
21 20 ralrimivv
22 sneq ${⊢}{h}={i}\to \left\{{h}\right\}=\left\{{i}\right\}$
23 22 fveq2d ${⊢}{h}={i}\to {J}\left(\left\{{h}\right\}\right)={J}\left(\left\{{i}\right\}\right)$
24 23 eqeq2d ${⊢}{h}={i}\to \left({M}\left({N}\left(\left\{{Y}\right\}\right)\right)={J}\left(\left\{{h}\right\}\right)↔{M}\left({N}\left(\left\{{Y}\right\}\right)\right)={J}\left(\left\{{i}\right\}\right)\right)$
25 oveq2 ${⊢}{h}={i}\to {G}{R}{h}={G}{R}{i}$
26 25 sneqd ${⊢}{h}={i}\to \left\{{G}{R}{h}\right\}=\left\{{G}{R}{i}\right\}$
27 26 fveq2d ${⊢}{h}={i}\to {J}\left(\left\{{G}{R}{h}\right\}\right)={J}\left(\left\{{G}{R}{i}\right\}\right)$
28 27 eqeq2d
29 24 28 anbi12d
30 29 reu4
31 18 21 30 sylanbrc