This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem dia1dim

Description: Two expressions for the 1-dimensional subspaces of partial vector space A (when F is a nonzero vector i.e. non-identity translation). Remark after Lemma L in Crawley p. 120 line 21. (Contributed by NM, 15-Oct-2013) (Revised by Mario Carneiro, 22-Jun-2014)

Ref Expression
Hypotheses dia1dim.h ⊢ H = LHyp ⁡ K
dia1dim.t ⊢ T = LTrn ⁡ K ⁡ W
dia1dim.r ⊢ R = trL ⁡ K ⁡ W
dia1dim.e ⊢ E = TEndo ⁡ K ⁡ W
dia1dim.i ⊢ I = DIsoA ⁡ K ⁡ W
Assertion dia1dim ⊢ K ∈ HL ∧ W ∈ H ∧ F ∈ T → I ⁡ R ⁡ F = g | ∃ s ∈ E g = s ⁡ F

Proof

Step Hyp Ref Expression
1 dia1dim.h ⊢ H = LHyp ⁡ K
2 dia1dim.t ⊢ T = LTrn ⁡ K ⁡ W
3 dia1dim.r ⊢ R = trL ⁡ K ⁡ W
4 dia1dim.e ⊢ E = TEndo ⁡ K ⁡ W
5 dia1dim.i ⊢ I = DIsoA ⁡ K ⁡ W
6 simpl ⊢ K ∈ HL ∧ W ∈ H ∧ F ∈ T → K ∈ HL ∧ W ∈ H
7 eqid ⊢ Base K = Base K
8 7 1 2 3 trlcl ⊢ K ∈ HL ∧ W ∈ H ∧ F ∈ T → R ⁡ F ∈ Base K
9 eqid ⊢ ≤ K = ≤ K
10 9 1 2 3 trlle ⊢ K ∈ HL ∧ W ∈ H ∧ F ∈ T → R ⁡ F ≤ K W
11 7 9 1 2 3 5 diaval ⊢ K ∈ HL ∧ W ∈ H ∧ R ⁡ F ∈ Base K ∧ R ⁡ F ≤ K W → I ⁡ R ⁡ F = g ∈ T | R ⁡ g ≤ K R ⁡ F
12 6 8 10 11 syl12anc ⊢ K ∈ HL ∧ W ∈ H ∧ F ∈ T → I ⁡ R ⁡ F = g ∈ T | R ⁡ g ≤ K R ⁡ F
13 9 1 2 3 4 dva1dim ⊢ K ∈ HL ∧ W ∈ H ∧ F ∈ T → g | ∃ s ∈ E g = s ⁡ F = g ∈ T | R ⁡ g ≤ K R ⁡ F
14 12 13 eqtr4d ⊢ K ∈ HL ∧ W ∈ H ∧ F ∈ T → I ⁡ R ⁡ F = g | ∃ s ∈ E g = s ⁡ F