Metamath Proof Explorer

Theorem dihmeetlem4preN

Description: Lemma for isomorphism H of a lattice meet. (Contributed by NM, 30-Mar-2014) (New usage is discouraged.)

Ref Expression
Hypotheses dihmeetlem4.b ${⊢}{B}={\mathrm{Base}}_{{K}}$
dihmeetlem4.l
dihmeetlem4.m
dihmeetlem4.a ${⊢}{A}=\mathrm{Atoms}\left({K}\right)$
dihmeetlem4.h ${⊢}{H}=\mathrm{LHyp}\left({K}\right)$
dihmeetlem4.i ${⊢}{I}=\mathrm{DIsoH}\left({K}\right)\left({W}\right)$
dihmeetlem4.u ${⊢}{U}=\mathrm{DVecH}\left({K}\right)\left({W}\right)$
dihmeetlem4.z
dihmeetlem4.g ${⊢}{G}=\left(\iota {g}\in {T}|{g}\left({P}\right)={Q}\right)$
dihmeetlem4.p ${⊢}{P}=\mathrm{oc}\left({K}\right)\left({W}\right)$
dihmeetlem4.t ${⊢}{T}=\mathrm{LTrn}\left({K}\right)\left({W}\right)$
dihmeetlem4.r ${⊢}{R}=\mathrm{trL}\left({K}\right)\left({W}\right)$
dihmeetlem4.e ${⊢}{E}=\mathrm{TEndo}\left({K}\right)\left({W}\right)$
dihmeetlem4.o ${⊢}{O}=\left({h}\in {T}⟼{\mathrm{I}↾}_{{B}}\right)$
Assertion dihmeetlem4preN

Proof

Step Hyp Ref Expression
1 dihmeetlem4.b ${⊢}{B}={\mathrm{Base}}_{{K}}$
2 dihmeetlem4.l
3 dihmeetlem4.m
4 dihmeetlem4.a ${⊢}{A}=\mathrm{Atoms}\left({K}\right)$
5 dihmeetlem4.h ${⊢}{H}=\mathrm{LHyp}\left({K}\right)$
6 dihmeetlem4.i ${⊢}{I}=\mathrm{DIsoH}\left({K}\right)\left({W}\right)$
7 dihmeetlem4.u ${⊢}{U}=\mathrm{DVecH}\left({K}\right)\left({W}\right)$
8 dihmeetlem4.z
9 dihmeetlem4.g ${⊢}{G}=\left(\iota {g}\in {T}|{g}\left({P}\right)={Q}\right)$
10 dihmeetlem4.p ${⊢}{P}=\mathrm{oc}\left({K}\right)\left({W}\right)$
11 dihmeetlem4.t ${⊢}{T}=\mathrm{LTrn}\left({K}\right)\left({W}\right)$
12 dihmeetlem4.r ${⊢}{R}=\mathrm{trL}\left({K}\right)\left({W}\right)$
13 dihmeetlem4.e ${⊢}{E}=\mathrm{TEndo}\left({K}\right)\left({W}\right)$
14 dihmeetlem4.o ${⊢}{O}=\left({h}\in {T}⟼{\mathrm{I}↾}_{{B}}\right)$
15 5 6 dihvalrel ${⊢}\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\to \mathrm{Rel}{I}\left({Q}\right)$
16 relin1
17 15 16 syl
19 5 6 dihvalrel ${⊢}\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\to \mathrm{Rel}{I}\left(\mathrm{0.}\left({K}\right)\right)$
20 eqid ${⊢}\mathrm{0.}\left({K}\right)=\mathrm{0.}\left({K}\right)$
21 20 5 6 7 8 dih0
22 21 releqd
23 19 22 mpbid
25 id
26 elin
27 vex ${⊢}{f}\in \mathrm{V}$
28 vex ${⊢}{s}\in \mathrm{V}$
29 2 4 5 10 11 13 6 9 27 28 dihopelvalcqat
31 simp1
32 simp1l
33 32 hllatd
34 simp2l
35 simp1r
36 1 5 lhpbase ${⊢}{W}\in {H}\to {W}\in {B}$
37 35 36 syl
38 1 3 latmcl
39 33 34 37 38 syl3anc
40 1 2 3 latmle2
41 33 34 37 40 syl3anc
42 1 2 5 11 12 14 6 dihopelvalbN
43 31 39 41 42 syl12anc
44 30 43 anbi12d
45 simprll
46 simprrr
47 46 fveq1d
48 simpl1
49 2 4 5 10 lhpocnel2
50 48 49 syl
51 simpl3
52 2 4 5 11 9 ltrniotacl
53 48 50 51 52 syl3anc
54 14 1 tendo02 ${⊢}{G}\in {T}\to {O}\left({G}\right)={\mathrm{I}↾}_{{B}}$
55 53 54 syl
56 45 47 55 3eqtrd
57 56 46 jca
58 simpl1
59 58 49 syl
60 simpl3
61 58 59 60 52 syl3anc
62 61 54 syl
63 simprr
64 63 fveq1d
65 simprl
66 62 64 65 3eqtr4rd
67 1 5 11 13 14 tendo0cl ${⊢}\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\to {O}\in {E}$
68 58 67 syl
69 63 68 eqeltrd
70 1 5 11 idltrn ${⊢}\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\to {\mathrm{I}↾}_{{B}}\in {T}$
71 58 70 syl
72 65 71 eqeltrd
73 65 fveq2d
74 1 20 5 12 trlid0 ${⊢}\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\to {R}\left({\mathrm{I}↾}_{{B}}\right)=\mathrm{0.}\left({K}\right)$
75 58 74 syl
76 73 75 eqtrd
77 simpl1l
78 hlatl ${⊢}{K}\in \mathrm{HL}\to {K}\in \mathrm{AtLat}$
79 77 78 syl
81 1 2 20 atl0le
82 79 80 81 syl2anc
83 76 82 eqbrtrd
84 72 83 63 jca31
85 66 69 84 jca31
86 57 85 impbida
87 44 86 bitrd
88 opex ${⊢}⟨{f},{s}⟩\in \mathrm{V}$
89 88 elsn ${⊢}⟨{f},{s}⟩\in \left\{⟨{\mathrm{I}↾}_{{B}},{O}⟩\right\}↔⟨{f},{s}⟩=⟨{\mathrm{I}↾}_{{B}},{O}⟩$
90 27 28 opth ${⊢}⟨{f},{s}⟩=⟨{\mathrm{I}↾}_{{B}},{O}⟩↔\left({f}={\mathrm{I}↾}_{{B}}\wedge {s}={O}\right)$
91 89 90 bitr2i ${⊢}\left({f}={\mathrm{I}↾}_{{B}}\wedge {s}={O}\right)↔⟨{f},{s}⟩\in \left\{⟨{\mathrm{I}↾}_{{B}},{O}⟩\right\}$
92 87 91 syl6bb
93 1 5 11 7 8 14 dvh0g