This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem cdlemeg47rv2

Description: Value of g_s(r) when r is an atom under pq and s is any atom not under pq, using very compact hypotheses. TODO: FIX COMMENT. (Contributed by NM, 1-Apr-2013)

Ref Expression
Hypotheses cdlemef47.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
cdlemef47.l ⊢ ≤ = ( le ‘ 𝐾 )
cdlemef47.j ⊢ ∨ = ( join ‘ 𝐾 )
cdlemef47.m ⊢ ∧ = ( meet ‘ 𝐾 )
cdlemef47.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
cdlemef47.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
cdlemef47.v ⊢ 𝑉 = ( ( 𝑄 ∨ 𝑃 ) ∧ 𝑊 )
cdlemef47.n ⊢ 𝑁 = ( ( 𝑣 ∨ 𝑉 ) ∧ ( 𝑃 ∨ ( ( 𝑄 ∨ 𝑣 ) ∧ 𝑊 ) ) )
cdlemefs47.o ⊢ 𝑂 = ( ( 𝑄 ∨ 𝑃 ) ∧ ( 𝑁 ∨ ( ( 𝑢 ∨ 𝑣 ) ∧ 𝑊 ) ) )
cdlemef47.g ⊢ 𝐺 = ( 𝑎 ∈ 𝐵 ↦ if ( ( 𝑄 ≠ 𝑃 ∧ ¬ 𝑎 ≤ 𝑊 ) , ( ℩ 𝑐 ∈ 𝐵 ∀ 𝑢 ∈ 𝐴 ( ( ¬ 𝑢 ≤ 𝑊 ∧ ( 𝑢 ∨ ( 𝑎 ∧ 𝑊 ) ) = 𝑎 ) → 𝑐 = ( if ( 𝑢 ≤ ( 𝑄 ∨ 𝑃 ) , ( ℩ 𝑏 ∈ 𝐵 ∀ 𝑣 ∈ 𝐴 ( ( ¬ 𝑣 ≤ 𝑊 ∧ ¬ 𝑣 ≤ ( 𝑄 ∨ 𝑃 ) ) → 𝑏 = 𝑂 ) ) , ⦋ 𝑢 / 𝑣 ⦌ 𝑁 ) ∨ ( 𝑎 ∧ 𝑊 ) ) ) ) , 𝑎 ) )
Assertion cdlemeg47rv2 ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ∧ ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ) ∧ ( 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ) ) → ( 𝐺 ‘ 𝑅 ) = ( ( 𝑄 ∨ 𝑃 ) ∧ ( ( 𝐺 ‘ 𝑆 ) ∨ ( ( 𝑅 ∨ 𝑆 ) ∧ 𝑊 ) ) ) )

Proof

Step Hyp Ref Expression
1 cdlemef47.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
2 cdlemef47.l ⊢ ≤ = ( le ‘ 𝐾 )
3 cdlemef47.j ⊢ ∨ = ( join ‘ 𝐾 )
4 cdlemef47.m ⊢ ∧ = ( meet ‘ 𝐾 )
5 cdlemef47.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
6 cdlemef47.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
7 cdlemef47.v ⊢ 𝑉 = ( ( 𝑄 ∨ 𝑃 ) ∧ 𝑊 )
8 cdlemef47.n ⊢ 𝑁 = ( ( 𝑣 ∨ 𝑉 ) ∧ ( 𝑃 ∨ ( ( 𝑄 ∨ 𝑣 ) ∧ 𝑊 ) ) )
9 cdlemefs47.o ⊢ 𝑂 = ( ( 𝑄 ∨ 𝑃 ) ∧ ( 𝑁 ∨ ( ( 𝑢 ∨ 𝑣 ) ∧ 𝑊 ) ) )
10 cdlemef47.g ⊢ 𝐺 = ( 𝑎 ∈ 𝐵 ↦ if ( ( 𝑄 ≠ 𝑃 ∧ ¬ 𝑎 ≤ 𝑊 ) , ( ℩ 𝑐 ∈ 𝐵 ∀ 𝑢 ∈ 𝐴 ( ( ¬ 𝑢 ≤ 𝑊 ∧ ( 𝑢 ∨ ( 𝑎 ∧ 𝑊 ) ) = 𝑎 ) → 𝑐 = ( if ( 𝑢 ≤ ( 𝑄 ∨ 𝑃 ) , ( ℩ 𝑏 ∈ 𝐵 ∀ 𝑣 ∈ 𝐴 ( ( ¬ 𝑣 ≤ 𝑊 ∧ ¬ 𝑣 ≤ ( 𝑄 ∨ 𝑃 ) ) → 𝑏 = 𝑂 ) ) , ⦋ 𝑢 / 𝑣 ⦌ 𝑁 ) ∨ ( 𝑎 ∧ 𝑊 ) ) ) ) , 𝑎 ) )
11 1 2 3 4 5 6 7 8 9 10 cdlemeg47rv ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ∧ ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ) ∧ ( 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ) ) → ( 𝐺 ‘ 𝑅 ) = ⦋ 𝑅 / 𝑢 ⦌ ⦋ 𝑆 / 𝑣 ⦌ 𝑂 )
12 simp22l ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ∧ ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ) ∧ ( 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ) ) → 𝑅 ∈ 𝐴 )
13 nfcvd ⊢ ( 𝑅 ∈ 𝐴 → Ⅎ 𝑢 ( ( 𝑄 ∨ 𝑃 ) ∧ ( ⦋ 𝑆 / 𝑣 ⦌ 𝑁 ∨ ( ( 𝑅 ∨ 𝑆 ) ∧ 𝑊 ) ) ) )
14 oveq1 ⊢ ( 𝑢 = 𝑅 → ( 𝑢 ∨ 𝑆 ) = ( 𝑅 ∨ 𝑆 ) )
15 14 oveq1d ⊢ ( 𝑢 = 𝑅 → ( ( 𝑢 ∨ 𝑆 ) ∧ 𝑊 ) = ( ( 𝑅 ∨ 𝑆 ) ∧ 𝑊 ) )
16 15 oveq2d ⊢ ( 𝑢 = 𝑅 → ( ⦋ 𝑆 / 𝑣 ⦌ 𝑁 ∨ ( ( 𝑢 ∨ 𝑆 ) ∧ 𝑊 ) ) = ( ⦋ 𝑆 / 𝑣 ⦌ 𝑁 ∨ ( ( 𝑅 ∨ 𝑆 ) ∧ 𝑊 ) ) )
17 16 oveq2d ⊢ ( 𝑢 = 𝑅 → ( ( 𝑄 ∨ 𝑃 ) ∧ ( ⦋ 𝑆 / 𝑣 ⦌ 𝑁 ∨ ( ( 𝑢 ∨ 𝑆 ) ∧ 𝑊 ) ) ) = ( ( 𝑄 ∨ 𝑃 ) ∧ ( ⦋ 𝑆 / 𝑣 ⦌ 𝑁 ∨ ( ( 𝑅 ∨ 𝑆 ) ∧ 𝑊 ) ) ) )
18 13 17 csbiegf ⊢ ( 𝑅 ∈ 𝐴 → ⦋ 𝑅 / 𝑢 ⦌ ( ( 𝑄 ∨ 𝑃 ) ∧ ( ⦋ 𝑆 / 𝑣 ⦌ 𝑁 ∨ ( ( 𝑢 ∨ 𝑆 ) ∧ 𝑊 ) ) ) = ( ( 𝑄 ∨ 𝑃 ) ∧ ( ⦋ 𝑆 / 𝑣 ⦌ 𝑁 ∨ ( ( 𝑅 ∨ 𝑆 ) ∧ 𝑊 ) ) ) )
19 12 18 syl ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ∧ ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ) ∧ ( 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ) ) → ⦋ 𝑅 / 𝑢 ⦌ ( ( 𝑄 ∨ 𝑃 ) ∧ ( ⦋ 𝑆 / 𝑣 ⦌ 𝑁 ∨ ( ( 𝑢 ∨ 𝑆 ) ∧ 𝑊 ) ) ) = ( ( 𝑄 ∨ 𝑃 ) ∧ ( ⦋ 𝑆 / 𝑣 ⦌ 𝑁 ∨ ( ( 𝑅 ∨ 𝑆 ) ∧ 𝑊 ) ) ) )
20 simp23l ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ∧ ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ) ∧ ( 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ) ) → 𝑆 ∈ 𝐴 )
21 eqid ⊢ ( ( 𝑄 ∨ 𝑃 ) ∧ ( ⦋ 𝑆 / 𝑣 ⦌ 𝑁 ∨ ( ( 𝑢 ∨ 𝑆 ) ∧ 𝑊 ) ) ) = ( ( 𝑄 ∨ 𝑃 ) ∧ ( ⦋ 𝑆 / 𝑣 ⦌ 𝑁 ∨ ( ( 𝑢 ∨ 𝑆 ) ∧ 𝑊 ) ) )
22 9 21 cdleme31se2 ⊢ ( 𝑆 ∈ 𝐴 → ⦋ 𝑆 / 𝑣 ⦌ 𝑂 = ( ( 𝑄 ∨ 𝑃 ) ∧ ( ⦋ 𝑆 / 𝑣 ⦌ 𝑁 ∨ ( ( 𝑢 ∨ 𝑆 ) ∧ 𝑊 ) ) ) )
23 20 22 syl ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ∧ ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ) ∧ ( 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ) ) → ⦋ 𝑆 / 𝑣 ⦌ 𝑂 = ( ( 𝑄 ∨ 𝑃 ) ∧ ( ⦋ 𝑆 / 𝑣 ⦌ 𝑁 ∨ ( ( 𝑢 ∨ 𝑆 ) ∧ 𝑊 ) ) ) )
24 23 csbeq2dv ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ∧ ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ) ∧ ( 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ) ) → ⦋ 𝑅 / 𝑢 ⦌ ⦋ 𝑆 / 𝑣 ⦌ 𝑂 = ⦋ 𝑅 / 𝑢 ⦌ ( ( 𝑄 ∨ 𝑃 ) ∧ ( ⦋ 𝑆 / 𝑣 ⦌ 𝑁 ∨ ( ( 𝑢 ∨ 𝑆 ) ∧ 𝑊 ) ) ) )
25 simp1 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ∧ ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ) ∧ ( 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ) ) → ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) )
26 simp21 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ∧ ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ) ∧ ( 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ) ) → 𝑃 ≠ 𝑄 )
27 simp23 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ∧ ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ) ∧ ( 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ) ) → ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) )
28 simp3r ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ∧ ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ) ∧ ( 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ) ) → ¬ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) )
29 1 2 3 4 5 6 7 8 9 10 cdlemeg47b ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ) ∧ ¬ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ) → ( 𝐺 ‘ 𝑆 ) = ⦋ 𝑆 / 𝑣 ⦌ 𝑁 )
30 25 26 27 28 29 syl121anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ∧ ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ) ∧ ( 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ) ) → ( 𝐺 ‘ 𝑆 ) = ⦋ 𝑆 / 𝑣 ⦌ 𝑁 )
31 30 oveq1d ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ∧ ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ) ∧ ( 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ) ) → ( ( 𝐺 ‘ 𝑆 ) ∨ ( ( 𝑅 ∨ 𝑆 ) ∧ 𝑊 ) ) = ( ⦋ 𝑆 / 𝑣 ⦌ 𝑁 ∨ ( ( 𝑅 ∨ 𝑆 ) ∧ 𝑊 ) ) )
32 31 oveq2d ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ∧ ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ) ∧ ( 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ) ) → ( ( 𝑄 ∨ 𝑃 ) ∧ ( ( 𝐺 ‘ 𝑆 ) ∨ ( ( 𝑅 ∨ 𝑆 ) ∧ 𝑊 ) ) ) = ( ( 𝑄 ∨ 𝑃 ) ∧ ( ⦋ 𝑆 / 𝑣 ⦌ 𝑁 ∨ ( ( 𝑅 ∨ 𝑆 ) ∧ 𝑊 ) ) ) )
33 19 24 32 3eqtr4d ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ∧ ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ) ∧ ( 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ) ) → ⦋ 𝑅 / 𝑢 ⦌ ⦋ 𝑆 / 𝑣 ⦌ 𝑂 = ( ( 𝑄 ∨ 𝑃 ) ∧ ( ( 𝐺 ‘ 𝑆 ) ∨ ( ( 𝑅 ∨ 𝑆 ) ∧ 𝑊 ) ) ) )
34 11 33 eqtrd ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ∧ ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ) ∧ ( 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ) ) → ( 𝐺 ‘ 𝑅 ) = ( ( 𝑄 ∨ 𝑃 ) ∧ ( ( 𝐺 ‘ 𝑆 ) ∨ ( ( 𝑅 ∨ 𝑆 ) ∧ 𝑊 ) ) ) )