Metamath Proof Explorer


Theorem dia2dimlem7

Description: Lemma for dia2dim . Eliminate ( FP ) =/= P condition. (Contributed by NM, 8-Sep-2014)

Ref Expression
Hypotheses dia2dimlem7.l = ( le ‘ 𝐾 )
dia2dimlem7.j = ( join ‘ 𝐾 )
dia2dimlem7.m = ( meet ‘ 𝐾 )
dia2dimlem7.a 𝐴 = ( Atoms ‘ 𝐾 )
dia2dimlem7.h 𝐻 = ( LHyp ‘ 𝐾 )
dia2dimlem7.t 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
dia2dimlem7.r 𝑅 = ( ( trL ‘ 𝐾 ) ‘ 𝑊 )
dia2dimlem7.y 𝑌 = ( ( DVecA ‘ 𝐾 ) ‘ 𝑊 )
dia2dimlem7.s 𝑆 = ( LSubSp ‘ 𝑌 )
dia2dimlem7.pl = ( LSSum ‘ 𝑌 )
dia2dimlem7.n 𝑁 = ( LSpan ‘ 𝑌 )
dia2dimlem7.i 𝐼 = ( ( DIsoA ‘ 𝐾 ) ‘ 𝑊 )
dia2dimlem7.q 𝑄 = ( ( 𝑃 𝑈 ) ( ( 𝐹𝑃 ) 𝑉 ) )
dia2dimlem7.k ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) )
dia2dimlem7.u ( 𝜑 → ( 𝑈𝐴𝑈 𝑊 ) )
dia2dimlem7.v ( 𝜑 → ( 𝑉𝐴𝑉 𝑊 ) )
dia2dimlem7.p ( 𝜑 → ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) )
dia2dimlem7.f ( 𝜑𝐹𝑇 )
dia2dimlem7.rf ( 𝜑 → ( 𝑅𝐹 ) ( 𝑈 𝑉 ) )
dia2dimlem7.uv ( 𝜑𝑈𝑉 )
dia2dimlem7.ru ( 𝜑 → ( 𝑅𝐹 ) ≠ 𝑈 )
dia2dimlem7.rv ( 𝜑 → ( 𝑅𝐹 ) ≠ 𝑉 )
Assertion dia2dimlem7 ( 𝜑𝐹 ∈ ( ( 𝐼𝑈 ) ( 𝐼𝑉 ) ) )

Proof

Step Hyp Ref Expression
1 dia2dimlem7.l = ( le ‘ 𝐾 )
2 dia2dimlem7.j = ( join ‘ 𝐾 )
3 dia2dimlem7.m = ( meet ‘ 𝐾 )
4 dia2dimlem7.a 𝐴 = ( Atoms ‘ 𝐾 )
5 dia2dimlem7.h 𝐻 = ( LHyp ‘ 𝐾 )
6 dia2dimlem7.t 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
7 dia2dimlem7.r 𝑅 = ( ( trL ‘ 𝐾 ) ‘ 𝑊 )
8 dia2dimlem7.y 𝑌 = ( ( DVecA ‘ 𝐾 ) ‘ 𝑊 )
9 dia2dimlem7.s 𝑆 = ( LSubSp ‘ 𝑌 )
10 dia2dimlem7.pl = ( LSSum ‘ 𝑌 )
11 dia2dimlem7.n 𝑁 = ( LSpan ‘ 𝑌 )
12 dia2dimlem7.i 𝐼 = ( ( DIsoA ‘ 𝐾 ) ‘ 𝑊 )
13 dia2dimlem7.q 𝑄 = ( ( 𝑃 𝑈 ) ( ( 𝐹𝑃 ) 𝑉 ) )
14 dia2dimlem7.k ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) )
15 dia2dimlem7.u ( 𝜑 → ( 𝑈𝐴𝑈 𝑊 ) )
16 dia2dimlem7.v ( 𝜑 → ( 𝑉𝐴𝑉 𝑊 ) )
17 dia2dimlem7.p ( 𝜑 → ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) )
18 dia2dimlem7.f ( 𝜑𝐹𝑇 )
19 dia2dimlem7.rf ( 𝜑 → ( 𝑅𝐹 ) ( 𝑈 𝑉 ) )
20 dia2dimlem7.uv ( 𝜑𝑈𝑉 )
21 dia2dimlem7.ru ( 𝜑 → ( 𝑅𝐹 ) ≠ 𝑈 )
22 dia2dimlem7.rv ( 𝜑 → ( 𝑅𝐹 ) ≠ 𝑉 )
23 eqid ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
24 23 1 4 5 6 ltrnideq ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝐹𝑇 ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ) → ( 𝐹 = ( I ↾ ( Base ‘ 𝐾 ) ) ↔ ( 𝐹𝑃 ) = 𝑃 ) )
25 14 18 17 24 syl3anc ( 𝜑 → ( 𝐹 = ( I ↾ ( Base ‘ 𝐾 ) ) ↔ ( 𝐹𝑃 ) = 𝑃 ) )
26 eqid ( 0g𝑌 ) = ( 0g𝑌 )
27 23 5 6 8 26 dva0g ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) → ( 0g𝑌 ) = ( I ↾ ( Base ‘ 𝐾 ) ) )
28 14 27 syl ( 𝜑 → ( 0g𝑌 ) = ( I ↾ ( Base ‘ 𝐾 ) ) )
29 5 8 dvalvec ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) → 𝑌 ∈ LVec )
30 lveclmod ( 𝑌 ∈ LVec → 𝑌 ∈ LMod )
31 14 29 30 3syl ( 𝜑𝑌 ∈ LMod )
32 15 simpld ( 𝜑𝑈𝐴 )
33 23 4 atbase ( 𝑈𝐴𝑈 ∈ ( Base ‘ 𝐾 ) )
34 32 33 syl ( 𝜑𝑈 ∈ ( Base ‘ 𝐾 ) )
35 15 simprd ( 𝜑𝑈 𝑊 )
36 23 1 5 8 12 9 dialss ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑈 ∈ ( Base ‘ 𝐾 ) ∧ 𝑈 𝑊 ) ) → ( 𝐼𝑈 ) ∈ 𝑆 )
37 14 34 35 36 syl12anc ( 𝜑 → ( 𝐼𝑈 ) ∈ 𝑆 )
38 16 simpld ( 𝜑𝑉𝐴 )
39 23 4 atbase ( 𝑉𝐴𝑉 ∈ ( Base ‘ 𝐾 ) )
40 38 39 syl ( 𝜑𝑉 ∈ ( Base ‘ 𝐾 ) )
41 16 simprd ( 𝜑𝑉 𝑊 )
42 23 1 5 8 12 9 dialss ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑉 ∈ ( Base ‘ 𝐾 ) ∧ 𝑉 𝑊 ) ) → ( 𝐼𝑉 ) ∈ 𝑆 )
43 14 40 41 42 syl12anc ( 𝜑 → ( 𝐼𝑉 ) ∈ 𝑆 )
44 9 10 lsmcl ( ( 𝑌 ∈ LMod ∧ ( 𝐼𝑈 ) ∈ 𝑆 ∧ ( 𝐼𝑉 ) ∈ 𝑆 ) → ( ( 𝐼𝑈 ) ( 𝐼𝑉 ) ) ∈ 𝑆 )
45 31 37 43 44 syl3anc ( 𝜑 → ( ( 𝐼𝑈 ) ( 𝐼𝑉 ) ) ∈ 𝑆 )
46 26 9 lss0cl ( ( 𝑌 ∈ LMod ∧ ( ( 𝐼𝑈 ) ( 𝐼𝑉 ) ) ∈ 𝑆 ) → ( 0g𝑌 ) ∈ ( ( 𝐼𝑈 ) ( 𝐼𝑉 ) ) )
47 31 45 46 syl2anc ( 𝜑 → ( 0g𝑌 ) ∈ ( ( 𝐼𝑈 ) ( 𝐼𝑉 ) ) )
48 28 47 eqeltrrd ( 𝜑 → ( I ↾ ( Base ‘ 𝐾 ) ) ∈ ( ( 𝐼𝑈 ) ( 𝐼𝑉 ) ) )
49 eleq1a ( ( I ↾ ( Base ‘ 𝐾 ) ) ∈ ( ( 𝐼𝑈 ) ( 𝐼𝑉 ) ) → ( 𝐹 = ( I ↾ ( Base ‘ 𝐾 ) ) → 𝐹 ∈ ( ( 𝐼𝑈 ) ( 𝐼𝑉 ) ) ) )
50 48 49 syl ( 𝜑 → ( 𝐹 = ( I ↾ ( Base ‘ 𝐾 ) ) → 𝐹 ∈ ( ( 𝐼𝑈 ) ( 𝐼𝑉 ) ) ) )
51 25 50 sylbird ( 𝜑 → ( ( 𝐹𝑃 ) = 𝑃𝐹 ∈ ( ( 𝐼𝑈 ) ( 𝐼𝑉 ) ) ) )
52 51 imp ( ( 𝜑 ∧ ( 𝐹𝑃 ) = 𝑃 ) → 𝐹 ∈ ( ( 𝐼𝑈 ) ( 𝐼𝑉 ) ) )
53 14 adantr ( ( 𝜑 ∧ ( 𝐹𝑃 ) ≠ 𝑃 ) → ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) )
54 15 adantr ( ( 𝜑 ∧ ( 𝐹𝑃 ) ≠ 𝑃 ) → ( 𝑈𝐴𝑈 𝑊 ) )
55 16 adantr ( ( 𝜑 ∧ ( 𝐹𝑃 ) ≠ 𝑃 ) → ( 𝑉𝐴𝑉 𝑊 ) )
56 17 adantr ( ( 𝜑 ∧ ( 𝐹𝑃 ) ≠ 𝑃 ) → ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) )
57 18 anim1i ( ( 𝜑 ∧ ( 𝐹𝑃 ) ≠ 𝑃 ) → ( 𝐹𝑇 ∧ ( 𝐹𝑃 ) ≠ 𝑃 ) )
58 19 adantr ( ( 𝜑 ∧ ( 𝐹𝑃 ) ≠ 𝑃 ) → ( 𝑅𝐹 ) ( 𝑈 𝑉 ) )
59 20 adantr ( ( 𝜑 ∧ ( 𝐹𝑃 ) ≠ 𝑃 ) → 𝑈𝑉 )
60 21 adantr ( ( 𝜑 ∧ ( 𝐹𝑃 ) ≠ 𝑃 ) → ( 𝑅𝐹 ) ≠ 𝑈 )
61 22 adantr ( ( 𝜑 ∧ ( 𝐹𝑃 ) ≠ 𝑃 ) → ( 𝑅𝐹 ) ≠ 𝑉 )
62 1 2 3 4 5 6 7 8 9 10 11 12 13 53 54 55 56 57 58 59 60 61 dia2dimlem6 ( ( 𝜑 ∧ ( 𝐹𝑃 ) ≠ 𝑃 ) → 𝐹 ∈ ( ( 𝐼𝑈 ) ( 𝐼𝑉 ) ) )
63 52 62 pm2.61dane ( 𝜑𝐹 ∈ ( ( 𝐼𝑈 ) ( 𝐼𝑉 ) ) )