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

Metamath Proof Explorer

Theorem dia2dimlem11

Description: Lemma for dia2dim . Convert ordering hypothesis on RF to subspace membership F e. ( I( U .\/ V ) ) . (Contributed by NM, 8-Sep-2014)

Ref Expression
Hypotheses dia2dimlem11.l ⊢ ≤ ˙ = ≤ K
dia2dimlem11.j ⊢ ∨ ˙ = join ⁡ K
dia2dimlem11.m ⊢ ∧ ˙ = meet ⁡ K
dia2dimlem11.a ⊢ A = Atoms ⁡ K
dia2dimlem11.h ⊢ H = LHyp ⁡ K
dia2dimlem11.t ⊢ T = LTrn ⁡ K ⁡ W
dia2dimlem11.r ⊢ R = trL ⁡ K ⁡ W
dia2dimlem11.y ⊢ Y = DVecA ⁡ K ⁡ W
dia2dimlem11.s ⊢ S = LSubSp ⁡ Y
dia2dimlem11.pl ⊢ ⊕ ˙ = LSSum ⁡ Y
dia2dimlem11.n ⊢ N = LSpan ⁡ Y
dia2dimlem11.i ⊢ I = DIsoA ⁡ K ⁡ W
dia2dimlem11.k ⊢ φ → K ∈ HL ∧ W ∈ H
dia2dimlem11.u ⊢ φ → U ∈ A ∧ U ≤ ˙ W
dia2dimlem11.v ⊢ φ → V ∈ A ∧ V ≤ ˙ W
dia2dimlem11.f ⊢ φ → F ∈ T
dia2dimlem11.uv ⊢ φ → U ≠ V
dia2dimlem11.fe ⊢ φ → F ∈ I ⁡ U ∨ ˙ V
Assertion dia2dimlem11 ⊢ φ → F ∈ I ⁡ U ⊕ ˙ I ⁡ V

Proof

Step Hyp Ref Expression
1 dia2dimlem11.l ⊢ ≤ ˙ = ≤ K
2 dia2dimlem11.j ⊢ ∨ ˙ = join ⁡ K
3 dia2dimlem11.m ⊢ ∧ ˙ = meet ⁡ K
4 dia2dimlem11.a ⊢ A = Atoms ⁡ K
5 dia2dimlem11.h ⊢ H = LHyp ⁡ K
6 dia2dimlem11.t ⊢ T = LTrn ⁡ K ⁡ W
7 dia2dimlem11.r ⊢ R = trL ⁡ K ⁡ W
8 dia2dimlem11.y ⊢ Y = DVecA ⁡ K ⁡ W
9 dia2dimlem11.s ⊢ S = LSubSp ⁡ Y
10 dia2dimlem11.pl ⊢ ⊕ ˙ = LSSum ⁡ Y
11 dia2dimlem11.n ⊢ N = LSpan ⁡ Y
12 dia2dimlem11.i ⊢ I = DIsoA ⁡ K ⁡ W
13 dia2dimlem11.k ⊢ φ → K ∈ HL ∧ W ∈ H
14 dia2dimlem11.u ⊢ φ → U ∈ A ∧ U ≤ ˙ W
15 dia2dimlem11.v ⊢ φ → V ∈ A ∧ V ≤ ˙ W
16 dia2dimlem11.f ⊢ φ → F ∈ T
17 dia2dimlem11.uv ⊢ φ → U ≠ V
18 dia2dimlem11.fe ⊢ φ → F ∈ I ⁡ U ∨ ˙ V
19 1 2 4 5 6 7 8 9 11 12 13 14 15 16 18 dia2dimlem10 ⊢ φ → R ⁡ F ≤ ˙ U ∨ ˙ V
20 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 19 17 dia2dimlem9 ⊢ φ → F ∈ I ⁡ U ⊕ ˙ I ⁡ V