Metamath Proof Explorer


Theorem dia2dimlem8

Description: Lemma for dia2dim . Eliminate no-longer used auxiliary atoms P and Q . (Contributed by NM, 8-Sep-2014)

Ref Expression
Hypotheses dia2dimlem8.l ˙ = K
dia2dimlem8.j ˙ = join K
dia2dimlem8.m ˙ = meet K
dia2dimlem8.a A = Atoms K
dia2dimlem8.h H = LHyp K
dia2dimlem8.t T = LTrn K W
dia2dimlem8.r R = trL K W
dia2dimlem8.y Y = DVecA K W
dia2dimlem8.s S = LSubSp Y
dia2dimlem8.pl ˙ = LSSum Y
dia2dimlem8.n N = LSpan Y
dia2dimlem8.i I = DIsoA K W
dia2dimlem8.k φ K HL W H
dia2dimlem8.u φ U A U ˙ W
dia2dimlem8.v φ V A V ˙ W
dia2dimlem8.f φ F T
dia2dimlem8.rf φ R F ˙ U ˙ V
dia2dimlem8.uv φ U V
dia2dimlem8.ru φ R F U
dia2dimlem8.rv φ R F V
Assertion dia2dimlem8 φ F I U ˙ I V

Proof

Step Hyp Ref Expression
1 dia2dimlem8.l ˙ = K
2 dia2dimlem8.j ˙ = join K
3 dia2dimlem8.m ˙ = meet K
4 dia2dimlem8.a A = Atoms K
5 dia2dimlem8.h H = LHyp K
6 dia2dimlem8.t T = LTrn K W
7 dia2dimlem8.r R = trL K W
8 dia2dimlem8.y Y = DVecA K W
9 dia2dimlem8.s S = LSubSp Y
10 dia2dimlem8.pl ˙ = LSSum Y
11 dia2dimlem8.n N = LSpan Y
12 dia2dimlem8.i I = DIsoA K W
13 dia2dimlem8.k φ K HL W H
14 dia2dimlem8.u φ U A U ˙ W
15 dia2dimlem8.v φ V A V ˙ W
16 dia2dimlem8.f φ F T
17 dia2dimlem8.rf φ R F ˙ U ˙ V
18 dia2dimlem8.uv φ U V
19 dia2dimlem8.ru φ R F U
20 dia2dimlem8.rv φ R F V
21 eqid oc K W ˙ U ˙ F oc K W ˙ V = oc K W ˙ U ˙ F oc K W ˙ V
22 eqid oc K = oc K
23 1 22 4 5 lhpocnel K HL W H oc K W A ¬ oc K W ˙ W
24 13 23 syl φ oc K W A ¬ oc K W ˙ W
25 1 2 3 4 5 6 7 8 9 10 11 12 21 13 14 15 24 16 17 18 19 20 dia2dimlem7 φ F I U ˙ I V