Metamath Proof Explorer


Theorem cdlemefs29cpre1N

Description: TODO: FIX COMMENT. (Contributed by NM, 26-Mar-2013) (New usage is discouraged.)

Ref Expression
Hypotheses cdlemefs32.b 𝐵 = ( Base ‘ 𝐾 )
cdlemefs32.l = ( le ‘ 𝐾 )
cdlemefs32.j = ( join ‘ 𝐾 )
cdlemefs32.m = ( meet ‘ 𝐾 )
cdlemefs32.a 𝐴 = ( Atoms ‘ 𝐾 )
cdlemefs32.h 𝐻 = ( LHyp ‘ 𝐾 )
cdlemefs32.u 𝑈 = ( ( 𝑃 𝑄 ) 𝑊 )
cdlemefs32.d 𝐷 = ( ( 𝑡 𝑈 ) ( 𝑄 ( ( 𝑃 𝑡 ) 𝑊 ) ) )
cdlemefs32.e 𝐸 = ( ( 𝑃 𝑄 ) ( 𝐷 ( ( 𝑠 𝑡 ) 𝑊 ) ) )
cdlemefs32.i 𝐼 = ( 𝑦𝐵𝑡𝐴 ( ( ¬ 𝑡 𝑊 ∧ ¬ 𝑡 ( 𝑃 𝑄 ) ) → 𝑦 = 𝐸 ) )
cdlemefs32.n 𝑁 = if ( 𝑠 ( 𝑃 𝑄 ) , 𝐼 , 𝐶 )
Assertion cdlemefs29cpre1N ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( 𝑃𝑄 ∧ ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ) ) ∧ 𝑅 ( 𝑃 𝑄 ) ) → ∃! 𝑧𝐵𝑠𝐴 ( ( ( ¬ 𝑠 𝑊𝑠 ( 𝑃 𝑄 ) ) ∧ ( 𝑠 ( 𝑅 𝑊 ) ) = 𝑅 ) → 𝑧 = ( 𝑁 ( 𝑅 𝑊 ) ) ) )

Proof

Step Hyp Ref Expression
1 cdlemefs32.b 𝐵 = ( Base ‘ 𝐾 )
2 cdlemefs32.l = ( le ‘ 𝐾 )
3 cdlemefs32.j = ( join ‘ 𝐾 )
4 cdlemefs32.m = ( meet ‘ 𝐾 )
5 cdlemefs32.a 𝐴 = ( Atoms ‘ 𝐾 )
6 cdlemefs32.h 𝐻 = ( LHyp ‘ 𝐾 )
7 cdlemefs32.u 𝑈 = ( ( 𝑃 𝑄 ) 𝑊 )
8 cdlemefs32.d 𝐷 = ( ( 𝑡 𝑈 ) ( 𝑄 ( ( 𝑃 𝑡 ) 𝑊 ) ) )
9 cdlemefs32.e 𝐸 = ( ( 𝑃 𝑄 ) ( 𝐷 ( ( 𝑠 𝑡 ) 𝑊 ) ) )
10 cdlemefs32.i 𝐼 = ( 𝑦𝐵𝑡𝐴 ( ( ¬ 𝑡 𝑊 ∧ ¬ 𝑡 ( 𝑃 𝑄 ) ) → 𝑦 = 𝐸 ) )
11 cdlemefs32.n 𝑁 = if ( 𝑠 ( 𝑃 𝑄 ) , 𝐼 , 𝐶 )
12 breq1 ( 𝑠 = 𝑅 → ( 𝑠 ( 𝑃 𝑄 ) ↔ 𝑅 ( 𝑃 𝑄 ) ) )
13 simp1 ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ 𝑃𝑄 ∧ ( 𝑠𝐴 ∧ ( ¬ 𝑠 𝑊𝑠 ( 𝑃 𝑄 ) ) ) ) → ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) )
14 simp3l ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ 𝑃𝑄 ∧ ( 𝑠𝐴 ∧ ( ¬ 𝑠 𝑊𝑠 ( 𝑃 𝑄 ) ) ) ) → 𝑠𝐴 )
15 simp3rl ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ 𝑃𝑄 ∧ ( 𝑠𝐴 ∧ ( ¬ 𝑠 𝑊𝑠 ( 𝑃 𝑄 ) ) ) ) → ¬ 𝑠 𝑊 )
16 14 15 jca ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ 𝑃𝑄 ∧ ( 𝑠𝐴 ∧ ( ¬ 𝑠 𝑊𝑠 ( 𝑃 𝑄 ) ) ) ) → ( 𝑠𝐴 ∧ ¬ 𝑠 𝑊 ) )
17 simp3rr ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ 𝑃𝑄 ∧ ( 𝑠𝐴 ∧ ( ¬ 𝑠 𝑊𝑠 ( 𝑃 𝑄 ) ) ) ) → 𝑠 ( 𝑃 𝑄 ) )
18 simp2 ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ 𝑃𝑄 ∧ ( 𝑠𝐴 ∧ ( ¬ 𝑠 𝑊𝑠 ( 𝑃 𝑄 ) ) ) ) → 𝑃𝑄 )
19 1 2 3 4 5 6 7 8 9 10 11 cdlemefs27cl ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( ( 𝑠𝐴 ∧ ¬ 𝑠 𝑊 ) ∧ 𝑠 ( 𝑃 𝑄 ) ∧ 𝑃𝑄 ) ) → 𝑁𝐵 )
20 13 16 17 18 19 syl13anc ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ 𝑃𝑄 ∧ ( 𝑠𝐴 ∧ ( ¬ 𝑠 𝑊𝑠 ( 𝑃 𝑄 ) ) ) ) → 𝑁𝐵 )
21 1 2 3 4 5 6 7 8 9 10 11 cdlemefs32snb ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( 𝑃𝑄 ∧ ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ) ) ∧ 𝑅 ( 𝑃 𝑄 ) ) → 𝑅 / 𝑠 𝑁𝐵 )
22 1 2 3 4 5 6 12 20 21 cdlemefrs29cpre1 ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( 𝑃𝑄 ∧ ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ) ) ∧ 𝑅 ( 𝑃 𝑄 ) ) → ∃! 𝑧𝐵𝑠𝐴 ( ( ( ¬ 𝑠 𝑊𝑠 ( 𝑃 𝑄 ) ) ∧ ( 𝑠 ( 𝑅 𝑊 ) ) = 𝑅 ) → 𝑧 = ( 𝑁 ( 𝑅 𝑊 ) ) ) )