Metamath Proof Explorer


Theorem dia2dimlem6

Description: Lemma for dia2dim . Eliminate auxiliary translations G and D . (Contributed by NM, 8-Sep-2014)

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

Proof

Step Hyp Ref Expression
1 dia2dimlem6.l ˙ = K
2 dia2dimlem6.j ˙ = join K
3 dia2dimlem6.m ˙ = meet K
4 dia2dimlem6.a A = Atoms K
5 dia2dimlem6.h H = LHyp K
6 dia2dimlem6.t T = LTrn K W
7 dia2dimlem6.r R = trL K W
8 dia2dimlem6.y Y = DVecA K W
9 dia2dimlem6.s S = LSubSp Y
10 dia2dimlem6.pl ˙ = LSSum Y
11 dia2dimlem6.n N = LSpan Y
12 dia2dimlem6.i I = DIsoA K W
13 dia2dimlem6.q Q = P ˙ U ˙ F P ˙ V
14 dia2dimlem6.k φ K HL W H
15 dia2dimlem6.u φ U A U ˙ W
16 dia2dimlem6.v φ V A V ˙ W
17 dia2dimlem6.p φ P A ¬ P ˙ W
18 dia2dimlem6.f φ F T F P P
19 dia2dimlem6.rf φ R F ˙ U ˙ V
20 dia2dimlem6.uv φ U V
21 dia2dimlem6.ru φ R F U
22 dia2dimlem6.rv φ R F V
23 1 2 3 4 5 6 7 13 14 15 16 17 18 19 20 21 dia2dimlem1 φ Q A ¬ Q ˙ W
24 18 simpld φ F T
25 1 4 5 6 ltrnel K HL W H F T P A ¬ P ˙ W F P A ¬ F P ˙ W
26 14 24 17 25 syl3anc φ F P A ¬ F P ˙ W
27 1 4 5 6 cdleme50ex K HL W H Q A ¬ Q ˙ W F P A ¬ F P ˙ W d T d Q = F P
28 14 23 26 27 syl3anc φ d T d Q = F P
29 1 4 5 6 cdleme50ex K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W g T g P = Q
30 14 17 23 29 syl3anc φ g T g P = Q
31 14 3ad2ant1 φ g T g P = Q d T d Q = F P K HL W H
32 15 3ad2ant1 φ g T g P = Q d T d Q = F P U A U ˙ W
33 16 3ad2ant1 φ g T g P = Q d T d Q = F P V A V ˙ W
34 17 3ad2ant1 φ g T g P = Q d T d Q = F P P A ¬ P ˙ W
35 18 3ad2ant1 φ g T g P = Q d T d Q = F P F T F P P
36 19 3ad2ant1 φ g T g P = Q d T d Q = F P R F ˙ U ˙ V
37 20 3ad2ant1 φ g T g P = Q d T d Q = F P U V
38 21 3ad2ant1 φ g T g P = Q d T d Q = F P R F U
39 22 3ad2ant1 φ g T g P = Q d T d Q = F P R F V
40 simp21 φ g T g P = Q d T d Q = F P g T
41 simp22 φ g T g P = Q d T d Q = F P g P = Q
42 simp23 φ g T g P = Q d T d Q = F P d T
43 simp3 φ g T g P = Q d T d Q = F P d Q = F P
44 1 2 3 4 5 6 7 8 9 10 11 12 13 31 32 33 34 35 36 37 38 39 40 41 42 43 dia2dimlem5 φ g T g P = Q d T d Q = F P F I U ˙ I V
45 44 3exp φ g T g P = Q d T d Q = F P F I U ˙ I V
46 45 3expd φ g T g P = Q d T d Q = F P F I U ˙ I V
47 46 rexlimdv φ g T g P = Q d T d Q = F P F I U ˙ I V
48 30 47 mpd φ d T d Q = F P F I U ˙ I V
49 48 rexlimdv φ d T d Q = F P F I U ˙ I V
50 28 49 mpd φ F I U ˙ I V