# Metamath Proof Explorer

## Theorem cdleme32fva

Description: Part of proof of Lemma D in Crawley p. 113. Value of F at an atom not under W . (Contributed by NM, 2-Mar-2013)

Ref Expression
Hypotheses cdleme32.b ${⊢}{B}={\mathrm{Base}}_{{K}}$
cdleme32.l
cdleme32.j
cdleme32.m
cdleme32.a ${⊢}{A}=\mathrm{Atoms}\left({K}\right)$
cdleme32.h ${⊢}{H}=\mathrm{LHyp}\left({K}\right)$
cdleme32.u
cdleme32.c
cdleme32.d
cdleme32.e
cdleme32.i
cdleme32.n
cdleme32.o
cdleme32.f
Assertion cdleme32fva

### Proof

Step Hyp Ref Expression
1 cdleme32.b ${⊢}{B}={\mathrm{Base}}_{{K}}$
2 cdleme32.l
3 cdleme32.j
4 cdleme32.m
5 cdleme32.a ${⊢}{A}=\mathrm{Atoms}\left({K}\right)$
6 cdleme32.h ${⊢}{H}=\mathrm{LHyp}\left({K}\right)$
7 cdleme32.u
8 cdleme32.c
9 cdleme32.d
10 cdleme32.e
11 cdleme32.i
12 cdleme32.n
13 cdleme32.o
14 cdleme32.f
15 simp2l
16 1 5 atbase ${⊢}{R}\in {A}\to {R}\in {B}$
17 15 16 syl
18 eqid
19 13 18 cdleme31so
20 17 19 syl
21 simp1
22 simp3
23 simp2
24 1 2 3 4 5 6 7 8 9 10 11 12 cdleme32snb
25 21 22 23 24 syl12anc
26 nfv
27 nfcsb1v
28 27 nfeq2
29 26 28 nfim
30 breq1
31 30 notbid
32 csbeq1a
33 32 eqeq2d
34 31 33 imbi12d
35 34 ax-gen
36 ceqsralt
37 29 35 36 mp3an12
40 simp11
41 eqid ${⊢}\mathrm{0.}\left({K}\right)=\mathrm{0.}\left({K}\right)$
42 2 4 41 5 6 lhpmat
43 40 23 42 syl2anc
45 44 oveq2d
46 simp11l
48 hlol ${⊢}{K}\in \mathrm{HL}\to {K}\in \mathrm{OL}$
49 47 48 syl
50 1 5 atbase ${⊢}{s}\in {A}\to {s}\in {B}$
52 1 3 41 olj01
53 49 51 52 syl2anc
54 45 53 eqtrd
55 54 eqeq1d
56 44 oveq2d
57 simpl11
58 simpl12
59 simpl13
60 simpr
61 simpl3
62 1 2 3 4 5 6 7 8 9 10 11 12 cdleme27cl
63 57 58 59 60 61 62 syl122anc
64 1 3 41 olj01
65 49 63 64 syl2anc
66 56 65 eqtrd
67 66 eqeq2d
68 55 67 imbi12d
69 68 expr
70 69 pm5.74d
71 impexp
72 bi2.04
73 70 71 72 3bitr4g
74 73 ralbidva
75 simp2r
76 biimt
77 75 76 syl
78 39 74 77 3bitr4d