Metamath Proof Explorer


Theorem cdlemefrs29cpre1

Description: TODO: FIX COMMENT. (Contributed by NM, 29-Mar-2013)

Ref Expression
Hypotheses cdlemefrs27.b 𝐵 = ( Base ‘ 𝐾 )
cdlemefrs27.l = ( le ‘ 𝐾 )
cdlemefrs27.j = ( join ‘ 𝐾 )
cdlemefrs27.m = ( meet ‘ 𝐾 )
cdlemefrs27.a 𝐴 = ( Atoms ‘ 𝐾 )
cdlemefrs27.h 𝐻 = ( LHyp ‘ 𝐾 )
cdlemefrs27.eq ( 𝑠 = 𝑅 → ( 𝜑𝜓 ) )
cdlemefrs27.nb ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ 𝑃𝑄 ∧ ( 𝑠𝐴 ∧ ( ¬ 𝑠 𝑊𝜑 ) ) ) → 𝑁𝐵 )
cdlemefrs27.rnb ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( 𝑃𝑄 ∧ ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ) ) ∧ 𝜓 ) → 𝑅 / 𝑠 𝑁𝐵 )
Assertion cdlemefrs29cpre1 ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( 𝑃𝑄 ∧ ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ) ) ∧ 𝜓 ) → ∃! 𝑧𝐵𝑠𝐴 ( ( ( ¬ 𝑠 𝑊𝜑 ) ∧ ( 𝑠 ( 𝑅 𝑊 ) ) = 𝑅 ) → 𝑧 = ( 𝑁 ( 𝑅 𝑊 ) ) ) )

Proof

Step Hyp Ref Expression
1 cdlemefrs27.b 𝐵 = ( Base ‘ 𝐾 )
2 cdlemefrs27.l = ( le ‘ 𝐾 )
3 cdlemefrs27.j = ( join ‘ 𝐾 )
4 cdlemefrs27.m = ( meet ‘ 𝐾 )
5 cdlemefrs27.a 𝐴 = ( Atoms ‘ 𝐾 )
6 cdlemefrs27.h 𝐻 = ( LHyp ‘ 𝐾 )
7 cdlemefrs27.eq ( 𝑠 = 𝑅 → ( 𝜑𝜓 ) )
8 cdlemefrs27.nb ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ 𝑃𝑄 ∧ ( 𝑠𝐴 ∧ ( ¬ 𝑠 𝑊𝜑 ) ) ) → 𝑁𝐵 )
9 cdlemefrs27.rnb ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( 𝑃𝑄 ∧ ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ) ) ∧ 𝜓 ) → 𝑅 / 𝑠 𝑁𝐵 )
10 1 2 3 4 5 6 7 8 9 cdlemefrs29bpre1 ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( 𝑃𝑄 ∧ ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ) ) ∧ 𝜓 ) → ∃ 𝑧𝐵𝑠𝐴 ( ( ( ¬ 𝑠 𝑊𝜑 ) ∧ ( 𝑠 ( 𝑅 𝑊 ) ) = 𝑅 ) → 𝑧 = ( 𝑁 ( 𝑅 𝑊 ) ) ) )
11 simp11 ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( 𝑃𝑄 ∧ ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ) ) ∧ 𝜓 ) → ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) )
12 simp2rl ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( 𝑃𝑄 ∧ ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ) ) ∧ 𝜓 ) → 𝑅𝐴 )
13 1 5 atbase ( 𝑅𝐴𝑅𝐵 )
14 12 13 syl ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( 𝑃𝑄 ∧ ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ) ) ∧ 𝜓 ) → 𝑅𝐵 )
15 simp2rr ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( 𝑃𝑄 ∧ ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ) ) ∧ 𝜓 ) → ¬ 𝑅 𝑊 )
16 1 2 3 4 5 6 lhpmcvr2 ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑅𝐵 ∧ ¬ 𝑅 𝑊 ) ) → ∃ 𝑠𝐴 ( ¬ 𝑠 𝑊 ∧ ( 𝑠 ( 𝑅 𝑊 ) ) = 𝑅 ) )
17 11 14 15 16 syl12anc ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( 𝑃𝑄 ∧ ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ) ) ∧ 𝜓 ) → ∃ 𝑠𝐴 ( ¬ 𝑠 𝑊 ∧ ( 𝑠 ( 𝑅 𝑊 ) ) = 𝑅 ) )
18 simpl3 ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( 𝑃𝑄 ∧ ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ) ) ∧ 𝜓 ) ∧ 𝑠𝐴 ) → 𝜓 )
19 7 pm5.32ri ( ( 𝜑𝑠 = 𝑅 ) ↔ ( 𝜓𝑠 = 𝑅 ) )
20 19 baibr ( 𝜓 → ( 𝑠 = 𝑅 ↔ ( 𝜑𝑠 = 𝑅 ) ) )
21 18 20 syl ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( 𝑃𝑄 ∧ ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ) ) ∧ 𝜓 ) ∧ 𝑠𝐴 ) → ( 𝑠 = 𝑅 ↔ ( 𝜑𝑠 = 𝑅 ) ) )
22 simp2r ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( 𝑃𝑄 ∧ ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ) ) ∧ 𝜓 ) → ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ) )
23 eqid ( 0. ‘ 𝐾 ) = ( 0. ‘ 𝐾 )
24 2 4 23 5 6 lhpmat ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ) ) → ( 𝑅 𝑊 ) = ( 0. ‘ 𝐾 ) )
25 11 22 24 syl2anc ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( 𝑃𝑄 ∧ ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ) ) ∧ 𝜓 ) → ( 𝑅 𝑊 ) = ( 0. ‘ 𝐾 ) )
26 25 adantr ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( 𝑃𝑄 ∧ ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ) ) ∧ 𝜓 ) ∧ 𝑠𝐴 ) → ( 𝑅 𝑊 ) = ( 0. ‘ 𝐾 ) )
27 26 oveq2d ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( 𝑃𝑄 ∧ ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ) ) ∧ 𝜓 ) ∧ 𝑠𝐴 ) → ( 𝑠 ( 𝑅 𝑊 ) ) = ( 𝑠 ( 0. ‘ 𝐾 ) ) )
28 simp11l ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( 𝑃𝑄 ∧ ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ) ) ∧ 𝜓 ) → 𝐾 ∈ HL )
29 hlol ( 𝐾 ∈ HL → 𝐾 ∈ OL )
30 28 29 syl ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( 𝑃𝑄 ∧ ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ) ) ∧ 𝜓 ) → 𝐾 ∈ OL )
31 1 5 atbase ( 𝑠𝐴𝑠𝐵 )
32 1 3 23 olj01 ( ( 𝐾 ∈ OL ∧ 𝑠𝐵 ) → ( 𝑠 ( 0. ‘ 𝐾 ) ) = 𝑠 )
33 30 31 32 syl2an ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( 𝑃𝑄 ∧ ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ) ) ∧ 𝜓 ) ∧ 𝑠𝐴 ) → ( 𝑠 ( 0. ‘ 𝐾 ) ) = 𝑠 )
34 27 33 eqtrd ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( 𝑃𝑄 ∧ ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ) ) ∧ 𝜓 ) ∧ 𝑠𝐴 ) → ( 𝑠 ( 𝑅 𝑊 ) ) = 𝑠 )
35 34 eqeq1d ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( 𝑃𝑄 ∧ ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ) ) ∧ 𝜓 ) ∧ 𝑠𝐴 ) → ( ( 𝑠 ( 𝑅 𝑊 ) ) = 𝑅𝑠 = 𝑅 ) )
36 35 anbi2d ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( 𝑃𝑄 ∧ ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ) ) ∧ 𝜓 ) ∧ 𝑠𝐴 ) → ( ( 𝜑 ∧ ( 𝑠 ( 𝑅 𝑊 ) ) = 𝑅 ) ↔ ( 𝜑𝑠 = 𝑅 ) ) )
37 21 35 36 3bitr4d ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( 𝑃𝑄 ∧ ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ) ) ∧ 𝜓 ) ∧ 𝑠𝐴 ) → ( ( 𝑠 ( 𝑅 𝑊 ) ) = 𝑅 ↔ ( 𝜑 ∧ ( 𝑠 ( 𝑅 𝑊 ) ) = 𝑅 ) ) )
38 37 anbi2d ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( 𝑃𝑄 ∧ ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ) ) ∧ 𝜓 ) ∧ 𝑠𝐴 ) → ( ( ¬ 𝑠 𝑊 ∧ ( 𝑠 ( 𝑅 𝑊 ) ) = 𝑅 ) ↔ ( ¬ 𝑠 𝑊 ∧ ( 𝜑 ∧ ( 𝑠 ( 𝑅 𝑊 ) ) = 𝑅 ) ) ) )
39 anass ( ( ( ¬ 𝑠 𝑊𝜑 ) ∧ ( 𝑠 ( 𝑅 𝑊 ) ) = 𝑅 ) ↔ ( ¬ 𝑠 𝑊 ∧ ( 𝜑 ∧ ( 𝑠 ( 𝑅 𝑊 ) ) = 𝑅 ) ) )
40 38 39 bitr4di ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( 𝑃𝑄 ∧ ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ) ) ∧ 𝜓 ) ∧ 𝑠𝐴 ) → ( ( ¬ 𝑠 𝑊 ∧ ( 𝑠 ( 𝑅 𝑊 ) ) = 𝑅 ) ↔ ( ( ¬ 𝑠 𝑊𝜑 ) ∧ ( 𝑠 ( 𝑅 𝑊 ) ) = 𝑅 ) ) )
41 40 rexbidva ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( 𝑃𝑄 ∧ ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ) ) ∧ 𝜓 ) → ( ∃ 𝑠𝐴 ( ¬ 𝑠 𝑊 ∧ ( 𝑠 ( 𝑅 𝑊 ) ) = 𝑅 ) ↔ ∃ 𝑠𝐴 ( ( ¬ 𝑠 𝑊𝜑 ) ∧ ( 𝑠 ( 𝑅 𝑊 ) ) = 𝑅 ) ) )
42 17 41 mpbid ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( 𝑃𝑄 ∧ ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ) ) ∧ 𝜓 ) → ∃ 𝑠𝐴 ( ( ¬ 𝑠 𝑊𝜑 ) ∧ ( 𝑠 ( 𝑅 𝑊 ) ) = 𝑅 ) )
43 reusv1 ( ∃ 𝑠𝐴 ( ( ¬ 𝑠 𝑊𝜑 ) ∧ ( 𝑠 ( 𝑅 𝑊 ) ) = 𝑅 ) → ( ∃! 𝑧𝐵𝑠𝐴 ( ( ( ¬ 𝑠 𝑊𝜑 ) ∧ ( 𝑠 ( 𝑅 𝑊 ) ) = 𝑅 ) → 𝑧 = ( 𝑁 ( 𝑅 𝑊 ) ) ) ↔ ∃ 𝑧𝐵𝑠𝐴 ( ( ( ¬ 𝑠 𝑊𝜑 ) ∧ ( 𝑠 ( 𝑅 𝑊 ) ) = 𝑅 ) → 𝑧 = ( 𝑁 ( 𝑅 𝑊 ) ) ) ) )
44 42 43 syl ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( 𝑃𝑄 ∧ ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ) ) ∧ 𝜓 ) → ( ∃! 𝑧𝐵𝑠𝐴 ( ( ( ¬ 𝑠 𝑊𝜑 ) ∧ ( 𝑠 ( 𝑅 𝑊 ) ) = 𝑅 ) → 𝑧 = ( 𝑁 ( 𝑅 𝑊 ) ) ) ↔ ∃ 𝑧𝐵𝑠𝐴 ( ( ( ¬ 𝑠 𝑊𝜑 ) ∧ ( 𝑠 ( 𝑅 𝑊 ) ) = 𝑅 ) → 𝑧 = ( 𝑁 ( 𝑅 𝑊 ) ) ) ) )
45 10 44 mpbird ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( 𝑃𝑄 ∧ ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ) ) ∧ 𝜓 ) → ∃! 𝑧𝐵𝑠𝐴 ( ( ( ¬ 𝑠 𝑊𝜑 ) ∧ ( 𝑠 ( 𝑅 𝑊 ) ) = 𝑅 ) → 𝑧 = ( 𝑁 ( 𝑅 𝑊 ) ) ) )