Metamath Proof Explorer


Theorem cdleme43frv1snN

Description: Value of [_ R / s ]_ N when -. R .<_ ( P .\/ Q ) . (Contributed by NM, 30-Mar-2013) (New usage is discouraged.)

Ref Expression
Hypotheses cdlemefr27.b 𝐵 = ( Base ‘ 𝐾 )
cdlemefr27.l = ( le ‘ 𝐾 )
cdlemefr27.j = ( join ‘ 𝐾 )
cdlemefr27.m = ( meet ‘ 𝐾 )
cdlemefr27.a 𝐴 = ( Atoms ‘ 𝐾 )
cdlemefr27.h 𝐻 = ( LHyp ‘ 𝐾 )
cdlemefr27.u 𝑈 = ( ( 𝑃 𝑄 ) 𝑊 )
cdlemefr27.c 𝐶 = ( ( 𝑠 𝑈 ) ( 𝑄 ( ( 𝑃 𝑠 ) 𝑊 ) ) )
cdlemefr27.n 𝑁 = if ( 𝑠 ( 𝑃 𝑄 ) , 𝐼 , 𝐶 )
cdleme43fr.x 𝑋 = ( ( 𝑅 𝑈 ) ( 𝑄 ( ( 𝑃 𝑅 ) 𝑊 ) ) )
Assertion cdleme43frv1snN ( ( 𝑅𝐴 ∧ ¬ 𝑅 ( 𝑃 𝑄 ) ) → 𝑅 / 𝑠 𝑁 = 𝑋 )

Proof

Step Hyp Ref Expression
1 cdlemefr27.b 𝐵 = ( Base ‘ 𝐾 )
2 cdlemefr27.l = ( le ‘ 𝐾 )
3 cdlemefr27.j = ( join ‘ 𝐾 )
4 cdlemefr27.m = ( meet ‘ 𝐾 )
5 cdlemefr27.a 𝐴 = ( Atoms ‘ 𝐾 )
6 cdlemefr27.h 𝐻 = ( LHyp ‘ 𝐾 )
7 cdlemefr27.u 𝑈 = ( ( 𝑃 𝑄 ) 𝑊 )
8 cdlemefr27.c 𝐶 = ( ( 𝑠 𝑈 ) ( 𝑄 ( ( 𝑃 𝑠 ) 𝑊 ) ) )
9 cdlemefr27.n 𝑁 = if ( 𝑠 ( 𝑃 𝑄 ) , 𝐼 , 𝐶 )
10 cdleme43fr.x 𝑋 = ( ( 𝑅 𝑈 ) ( 𝑄 ( ( 𝑃 𝑅 ) 𝑊 ) ) )
11 8 9 10 cdleme31sn2 ( ( 𝑅𝐴 ∧ ¬ 𝑅 ( 𝑃 𝑄 ) ) → 𝑅 / 𝑠 𝑁 = 𝑋 )