# 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 = ( LHyp ` K )`
mapdpg.m
`|- M = ( ( mapd ` K ) ` W )`
mapdpg.u
`|- U = ( ( DVecH ` K ) ` W )`
mapdpg.v
`|- V = ( Base ` U )`
mapdpg.s
`|- .- = ( -g ` U )`
mapdpg.z
`|- .0. = ( 0g ` U )`
mapdpg.n
`|- N = ( LSpan ` U )`
mapdpg.c
`|- C = ( ( LCDual ` K ) ` W )`
mapdpg.f
`|- F = ( Base ` C )`
mapdpg.r
`|- R = ( -g ` C )`
mapdpg.j
`|- J = ( LSpan ` C )`
mapdpg.k
`|- ( ph -> ( K e. HL /\ W e. H ) )`
mapdpg.x
`|- ( ph -> X e. ( V \ { .0. } ) )`
mapdpg.y
`|- ( ph -> Y e. ( V \ { .0. } ) )`
mapdpg.g
`|- ( ph -> G e. F )`
mapdpg.ne
`|- ( ph -> ( N ` { X } ) =/= ( N ` { Y } ) )`
mapdpg.e
`|- ( ph -> ( M ` ( N ` { X } ) ) = ( J ` { G } ) )`
Assertion mapdpg
`|- ( ph -> E! h e. F ( ( M ` ( N ` { Y } ) ) = ( J ` { h } ) /\ ( M ` ( N ` { ( X .- Y ) } ) ) = ( J ` { ( G R h ) } ) ) )`

### Proof

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