Metamath Proof Explorer


Theorem dia2dimlem9

Description: Lemma for dia2dim . Eliminate ( RF ) =/= U , V conditions. (Contributed by NM, 8-Sep-2014)

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

Proof

Step Hyp Ref Expression
1 dia2dimlem9.l ˙ = K
2 dia2dimlem9.j ˙ = join K
3 dia2dimlem9.m ˙ = meet K
4 dia2dimlem9.a A = Atoms K
5 dia2dimlem9.h H = LHyp K
6 dia2dimlem9.t T = LTrn K W
7 dia2dimlem9.r R = trL K W
8 dia2dimlem9.y Y = DVecA K W
9 dia2dimlem9.s S = LSubSp Y
10 dia2dimlem9.pl ˙ = LSSum Y
11 dia2dimlem9.n N = LSpan Y
12 dia2dimlem9.i I = DIsoA K W
13 dia2dimlem9.k φ K HL W H
14 dia2dimlem9.u φ U A U ˙ W
15 dia2dimlem9.v φ V A V ˙ W
16 dia2dimlem9.f φ F T
17 dia2dimlem9.rf φ R F ˙ U ˙ V
18 dia2dimlem9.uv φ U V
19 5 8 dvalvec K HL W H Y LVec
20 lveclmod Y LVec Y LMod
21 9 lsssssubg Y LMod S SubGrp Y
22 13 19 20 21 4syl φ S SubGrp Y
23 14 simpld φ U A
24 eqid Base K = Base K
25 24 4 atbase U A U Base K
26 23 25 syl φ U Base K
27 14 simprd φ U ˙ W
28 24 1 5 8 12 9 dialss K HL W H U Base K U ˙ W I U S
29 13 26 27 28 syl12anc φ I U S
30 22 29 sseldd φ I U SubGrp Y
31 15 simpld φ V A
32 24 4 atbase V A V Base K
33 31 32 syl φ V Base K
34 15 simprd φ V ˙ W
35 24 1 5 8 12 9 dialss K HL W H V Base K V ˙ W I V S
36 13 33 34 35 syl12anc φ I V S
37 22 36 sseldd φ I V SubGrp Y
38 10 lsmub1 I U SubGrp Y I V SubGrp Y I U I U ˙ I V
39 30 37 38 syl2anc φ I U I U ˙ I V
40 39 adantr φ R F = U I U I U ˙ I V
41 5 6 7 12 dia1dimid K HL W H F T F I R F
42 13 16 41 syl2anc φ F I R F
43 42 adantr φ R F = U F I R F
44 fveq2 R F = U I R F = I U
45 44 adantl φ R F = U I R F = I U
46 43 45 eleqtrd φ R F = U F I U
47 40 46 sseldd φ R F = U F I U ˙ I V
48 30 adantr φ R F = V I U SubGrp Y
49 37 adantr φ R F = V I V SubGrp Y
50 10 lsmub2 I U SubGrp Y I V SubGrp Y I V I U ˙ I V
51 48 49 50 syl2anc φ R F = V I V I U ˙ I V
52 42 adantr φ R F = V F I R F
53 fveq2 R F = V I R F = I V
54 53 adantl φ R F = V I R F = I V
55 52 54 eleqtrd φ R F = V F I V
56 51 55 sseldd φ R F = V F I U ˙ I V
57 13 adantr φ R F U R F V K HL W H
58 14 adantr φ R F U R F V U A U ˙ W
59 15 adantr φ R F U R F V V A V ˙ W
60 16 adantr φ R F U R F V F T
61 17 adantr φ R F U R F V R F ˙ U ˙ V
62 18 adantr φ R F U R F V U V
63 simprl φ R F U R F V R F U
64 simprr φ R F U R F V R F V
65 1 2 3 4 5 6 7 8 9 10 11 12 57 58 59 60 61 62 63 64 dia2dimlem8 φ R F U R F V F I U ˙ I V
66 47 56 65 pm2.61da2ne φ F I U ˙ I V