Metamath Proof Explorer


Theorem cdlemefrs32fva

Description: Part of proof of Lemma E in Crawley p. 113. Value of F at an atom not under W . TODO: FIX COMMENT. TODO: consolidate uses of lhpmat here and elsewhere, and presence/absence of s .<_ ( P .\/ Q ) term. Also, why can proof be shortened with cdleme29cl ? What is difference from cdlemefs27cl ? (Contributed by NM, 29-Mar-2013)

Ref Expression
Hypotheses cdlemefrs27.b B=BaseK
cdlemefrs27.l ˙=K
cdlemefrs27.j ˙=joinK
cdlemefrs27.m ˙=meetK
cdlemefrs27.a A=AtomsK
cdlemefrs27.h H=LHypK
cdlemefrs27.eq s=Rφψ
cdlemefrs27.nb KHLWHPA¬P˙WQA¬Q˙WPQsA¬s˙WφNB
cdlemefrs27.rnb KHLWHPA¬P˙WQA¬Q˙WPQRA¬R˙WψR/sNB
cdleme29frs.o O=ιzB|sA¬s˙Ws˙x˙W=xz=N˙x˙W
Assertion cdlemefrs32fva KHLWHPA¬P˙WQA¬Q˙WPQRA¬R˙WψR/xO=R/sN

Proof

Step Hyp Ref Expression
1 cdlemefrs27.b B=BaseK
2 cdlemefrs27.l ˙=K
3 cdlemefrs27.j ˙=joinK
4 cdlemefrs27.m ˙=meetK
5 cdlemefrs27.a A=AtomsK
6 cdlemefrs27.h H=LHypK
7 cdlemefrs27.eq s=Rφψ
8 cdlemefrs27.nb KHLWHPA¬P˙WQA¬Q˙WPQsA¬s˙WφNB
9 cdlemefrs27.rnb KHLWHPA¬P˙WQA¬Q˙WPQRA¬R˙WψR/sNB
10 cdleme29frs.o O=ιzB|sA¬s˙Ws˙x˙W=xz=N˙x˙W
11 simp2rl KHLWHPA¬P˙WQA¬Q˙WPQRA¬R˙WψRA
12 1 5 atbase RARB
13 eqid ιzB|sA¬s˙Ws˙R˙W=Rz=N˙R˙W=ιzB|sA¬s˙Ws˙R˙W=Rz=N˙R˙W
14 10 13 cdleme31so RBR/xO=ιzB|sA¬s˙Ws˙R˙W=Rz=N˙R˙W
15 11 12 14 3syl KHLWHPA¬P˙WQA¬Q˙WPQRA¬R˙WψR/xO=ιzB|sA¬s˙Ws˙R˙W=Rz=N˙R˙W
16 ssidd KHLWHPA¬P˙WQA¬Q˙WPQRA¬R˙WψBB
17 simpll ¬s˙Wφs˙R˙W=R¬s˙W
18 simpr ¬s˙Wφs˙R˙W=Rs˙R˙W=R
19 17 18 jca ¬s˙Wφs˙R˙W=R¬s˙Ws˙R˙W=R
20 19 imim1i ¬s˙Ws˙R˙W=Rz=N˙R˙W¬s˙Wφs˙R˙W=Rz=N˙R˙W
21 20 ralimi sA¬s˙Ws˙R˙W=Rz=N˙R˙WsA¬s˙Wφs˙R˙W=Rz=N˙R˙W
22 21 rgenw zBsA¬s˙Ws˙R˙W=Rz=N˙R˙WsA¬s˙Wφs˙R˙W=Rz=N˙R˙W
23 22 a1i KHLWHPA¬P˙WQA¬Q˙WPQRA¬R˙WψzBsA¬s˙Ws˙R˙W=Rz=N˙R˙WsA¬s˙Wφs˙R˙W=Rz=N˙R˙W
24 1 2 3 4 5 6 7 8 9 cdlemefrs29bpre1 KHLWHPA¬P˙WQA¬Q˙WPQRA¬R˙WψzBsA¬s˙Wφs˙R˙W=Rz=N˙R˙W
25 simpl11 KHLWHPA¬P˙WQA¬Q˙WPQRA¬R˙WψsAKHLWH
26 simpl2r KHLWHPA¬P˙WQA¬Q˙WPQRA¬R˙WψsARA¬R˙W
27 simpl3 KHLWHPA¬P˙WQA¬Q˙WPQRA¬R˙WψsAψ
28 simpr KHLWHPA¬P˙WQA¬Q˙WPQRA¬R˙WψsAsA
29 1 2 3 4 5 6 7 cdlemefrs29pre00 KHLWHRA¬R˙WψsA¬s˙Wφs˙R˙W=R¬s˙Ws˙R˙W=R
30 25 26 27 28 29 syl31anc KHLWHPA¬P˙WQA¬Q˙WPQRA¬R˙WψsA¬s˙Wφs˙R˙W=R¬s˙Ws˙R˙W=R
31 30 imbi1d KHLWHPA¬P˙WQA¬Q˙WPQRA¬R˙WψsA¬s˙Wφs˙R˙W=Rz=N˙R˙W¬s˙Ws˙R˙W=Rz=N˙R˙W
32 31 ralbidva KHLWHPA¬P˙WQA¬Q˙WPQRA¬R˙WψsA¬s˙Wφs˙R˙W=Rz=N˙R˙WsA¬s˙Ws˙R˙W=Rz=N˙R˙W
33 32 rexbidv KHLWHPA¬P˙WQA¬Q˙WPQRA¬R˙WψzBsA¬s˙Wφs˙R˙W=Rz=N˙R˙WzBsA¬s˙Ws˙R˙W=Rz=N˙R˙W
34 24 33 mpbid KHLWHPA¬P˙WQA¬Q˙WPQRA¬R˙WψzBsA¬s˙Ws˙R˙W=Rz=N˙R˙W
35 1 2 3 4 5 6 7 8 9 cdlemefrs29cpre1 KHLWHPA¬P˙WQA¬Q˙WPQRA¬R˙Wψ∃!zBsA¬s˙Wφs˙R˙W=Rz=N˙R˙W
36 riotass2 BBzBsA¬s˙Ws˙R˙W=Rz=N˙R˙WsA¬s˙Wφs˙R˙W=Rz=N˙R˙WzBsA¬s˙Ws˙R˙W=Rz=N˙R˙W∃!zBsA¬s˙Wφs˙R˙W=Rz=N˙R˙WιzB|sA¬s˙Ws˙R˙W=Rz=N˙R˙W=ιzB|sA¬s˙Wφs˙R˙W=Rz=N˙R˙W
37 16 23 34 35 36 syl22anc KHLWHPA¬P˙WQA¬Q˙WPQRA¬R˙WψιzB|sA¬s˙Ws˙R˙W=Rz=N˙R˙W=ιzB|sA¬s˙Wφs˙R˙W=Rz=N˙R˙W
38 1 2 3 4 5 6 7 8 cdlemefrs29bpre0 KHLWHPA¬P˙WQA¬Q˙WPQRA¬R˙WψsA¬s˙Wφs˙R˙W=Rz=N˙R˙Wz=R/sN
39 38 adantr KHLWHPA¬P˙WQA¬Q˙WPQRA¬R˙WψzBsA¬s˙Wφs˙R˙W=Rz=N˙R˙Wz=R/sN
40 9 39 riota5 KHLWHPA¬P˙WQA¬Q˙WPQRA¬R˙WψιzB|sA¬s˙Wφs˙R˙W=Rz=N˙R˙W=R/sN
41 15 37 40 3eqtrd KHLWHPA¬P˙WQA¬Q˙WPQRA¬R˙WψR/xO=R/sN