Metamath Proof Explorer


Theorem dva1dim

Description: Two expressions for the 1-dimensional subspaces of partial vector space A. Remark in Crawley p. 120 line 21, but using a non-identity translation (nonzero vector) F whose trace is P rather than P itself; F exists by cdlemf . E is the division ring base by erngdv , and sF is the scalar product by dvavsca . F must be a non-identity translation for the expression to be a 1-dimensional subspace, although the theorem doesn't require it. (Contributed by NM, 14-Oct-2013)

Ref Expression
Hypotheses dva1dim.l ˙ = K
dva1dim.h H = LHyp K
dva1dim.t T = LTrn K W
dva1dim.r R = trL K W
dva1dim.e E = TEndo K W
Assertion dva1dim K HL W H F T g | s E g = s F = g T | R g ˙ R F

Proof

Step Hyp Ref Expression
1 dva1dim.l ˙ = K
2 dva1dim.h H = LHyp K
3 dva1dim.t T = LTrn K W
4 dva1dim.r R = trL K W
5 dva1dim.e E = TEndo K W
6 2 3 5 tendocl K HL W H s E F T s F T
7 1 2 3 4 5 tendotp K HL W H s E F T R s F ˙ R F
8 6 7 jca K HL W H s E F T s F T R s F ˙ R F
9 8 3expb K HL W H s E F T s F T R s F ˙ R F
10 9 anass1rs K HL W H F T s E s F T R s F ˙ R F
11 eleq1 g = s F g T s F T
12 fveq2 g = s F R g = R s F
13 12 breq1d g = s F R g ˙ R F R s F ˙ R F
14 11 13 anbi12d g = s F g T R g ˙ R F s F T R s F ˙ R F
15 10 14 syl5ibrcom K HL W H F T s E g = s F g T R g ˙ R F
16 15 rexlimdva K HL W H F T s E g = s F g T R g ˙ R F
17 simpll K HL W H F T g T R g ˙ R F K HL W H
18 simplr K HL W H F T g T R g ˙ R F F T
19 simprl K HL W H F T g T R g ˙ R F g T
20 simprr K HL W H F T g T R g ˙ R F R g ˙ R F
21 1 2 3 4 5 tendoex K HL W H F T g T R g ˙ R F s E s F = g
22 17 18 19 20 21 syl121anc K HL W H F T g T R g ˙ R F s E s F = g
23 eqcom s F = g g = s F
24 23 rexbii s E s F = g s E g = s F
25 22 24 sylib K HL W H F T g T R g ˙ R F s E g = s F
26 25 ex K HL W H F T g T R g ˙ R F s E g = s F
27 16 26 impbid K HL W H F T s E g = s F g T R g ˙ R F
28 27 abbidv K HL W H F T g | s E g = s F = g | g T R g ˙ R F
29 df-rab g T | R g ˙ R F = g | g T R g ˙ R F
30 28 29 eqtr4di K HL W H F T g | s E g = s F = g T | R g ˙ R F