Metamath Proof Explorer


Theorem cdlemg2klem

Description: cdleme42keg with simpler hypotheses. TODO: FIX COMMENT. (Contributed by NM, 22-Apr-2013)

Ref Expression
Hypotheses cdlemg2.b 𝐵 = ( Base ‘ 𝐾 )
cdlemg2.l = ( le ‘ 𝐾 )
cdlemg2.j = ( join ‘ 𝐾 )
cdlemg2.m = ( meet ‘ 𝐾 )
cdlemg2.a 𝐴 = ( Atoms ‘ 𝐾 )
cdlemg2.h 𝐻 = ( LHyp ‘ 𝐾 )
cdlemg2.t 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
cdlemg2ex.u 𝑈 = ( ( 𝑝 𝑞 ) 𝑊 )
cdlemg2ex.d 𝐷 = ( ( 𝑡 𝑈 ) ( 𝑞 ( ( 𝑝 𝑡 ) 𝑊 ) ) )
cdlemg2ex.e 𝐸 = ( ( 𝑝 𝑞 ) ( 𝐷 ( ( 𝑠 𝑡 ) 𝑊 ) ) )
cdlemg2ex.g 𝐺 = ( 𝑥𝐵 ↦ if ( ( 𝑝𝑞 ∧ ¬ 𝑥 𝑊 ) , ( 𝑧𝐵𝑠𝐴 ( ( ¬ 𝑠 𝑊 ∧ ( 𝑠 ( 𝑥 𝑊 ) ) = 𝑥 ) → 𝑧 = ( if ( 𝑠 ( 𝑝 𝑞 ) , ( 𝑦𝐵𝑡𝐴 ( ( ¬ 𝑡 𝑊 ∧ ¬ 𝑡 ( 𝑝 𝑞 ) ) → 𝑦 = 𝐸 ) ) , 𝑠 / 𝑡 𝐷 ) ( 𝑥 𝑊 ) ) ) ) , 𝑥 ) )
cdlemg2klem.v 𝑉 = ( ( 𝑃 𝑄 ) 𝑊 )
Assertion cdlemg2klem ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ 𝐹𝑇 ) → ( ( 𝐹𝑃 ) ( 𝐹𝑄 ) ) = ( ( 𝐹𝑃 ) 𝑉 ) )

Proof

Step Hyp Ref Expression
1 cdlemg2.b 𝐵 = ( Base ‘ 𝐾 )
2 cdlemg2.l = ( le ‘ 𝐾 )
3 cdlemg2.j = ( join ‘ 𝐾 )
4 cdlemg2.m = ( meet ‘ 𝐾 )
5 cdlemg2.a 𝐴 = ( Atoms ‘ 𝐾 )
6 cdlemg2.h 𝐻 = ( LHyp ‘ 𝐾 )
7 cdlemg2.t 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
8 cdlemg2ex.u 𝑈 = ( ( 𝑝 𝑞 ) 𝑊 )
9 cdlemg2ex.d 𝐷 = ( ( 𝑡 𝑈 ) ( 𝑞 ( ( 𝑝 𝑡 ) 𝑊 ) ) )
10 cdlemg2ex.e 𝐸 = ( ( 𝑝 𝑞 ) ( 𝐷 ( ( 𝑠 𝑡 ) 𝑊 ) ) )
11 cdlemg2ex.g 𝐺 = ( 𝑥𝐵 ↦ if ( ( 𝑝𝑞 ∧ ¬ 𝑥 𝑊 ) , ( 𝑧𝐵𝑠𝐴 ( ( ¬ 𝑠 𝑊 ∧ ( 𝑠 ( 𝑥 𝑊 ) ) = 𝑥 ) → 𝑧 = ( if ( 𝑠 ( 𝑝 𝑞 ) , ( 𝑦𝐵𝑡𝐴 ( ( ¬ 𝑡 𝑊 ∧ ¬ 𝑡 ( 𝑝 𝑞 ) ) → 𝑦 = 𝐸 ) ) , 𝑠 / 𝑡 𝐷 ) ( 𝑥 𝑊 ) ) ) ) , 𝑥 ) )
12 cdlemg2klem.v 𝑉 = ( ( 𝑃 𝑄 ) 𝑊 )
13 fveq1 ( 𝐹 = 𝐺 → ( 𝐹𝑃 ) = ( 𝐺𝑃 ) )
14 fveq1 ( 𝐹 = 𝐺 → ( 𝐹𝑄 ) = ( 𝐺𝑄 ) )
15 13 14 oveq12d ( 𝐹 = 𝐺 → ( ( 𝐹𝑃 ) ( 𝐹𝑄 ) ) = ( ( 𝐺𝑃 ) ( 𝐺𝑄 ) ) )
16 13 oveq1d ( 𝐹 = 𝐺 → ( ( 𝐹𝑃 ) 𝑉 ) = ( ( 𝐺𝑃 ) 𝑉 ) )
17 15 16 eqeq12d ( 𝐹 = 𝐺 → ( ( ( 𝐹𝑃 ) ( 𝐹𝑄 ) ) = ( ( 𝐹𝑃 ) 𝑉 ) ↔ ( ( 𝐺𝑃 ) ( 𝐺𝑄 ) ) = ( ( 𝐺𝑃 ) 𝑉 ) ) )
18 vex 𝑠 ∈ V
19 eqid ( ( 𝑠 𝑈 ) ( 𝑞 ( ( 𝑝 𝑠 ) 𝑊 ) ) ) = ( ( 𝑠 𝑈 ) ( 𝑞 ( ( 𝑝 𝑠 ) 𝑊 ) ) )
20 9 19 cdleme31sc ( 𝑠 ∈ V → 𝑠 / 𝑡 𝐷 = ( ( 𝑠 𝑈 ) ( 𝑞 ( ( 𝑝 𝑠 ) 𝑊 ) ) ) )
21 18 20 ax-mp 𝑠 / 𝑡 𝐷 = ( ( 𝑠 𝑈 ) ( 𝑞 ( ( 𝑝 𝑠 ) 𝑊 ) ) )
22 eqid ( 𝑦𝐵𝑡𝐴 ( ( ¬ 𝑡 𝑊 ∧ ¬ 𝑡 ( 𝑝 𝑞 ) ) → 𝑦 = 𝐸 ) ) = ( 𝑦𝐵𝑡𝐴 ( ( ¬ 𝑡 𝑊 ∧ ¬ 𝑡 ( 𝑝 𝑞 ) ) → 𝑦 = 𝐸 ) )
23 eqid if ( 𝑠 ( 𝑝 𝑞 ) , ( 𝑦𝐵𝑡𝐴 ( ( ¬ 𝑡 𝑊 ∧ ¬ 𝑡 ( 𝑝 𝑞 ) ) → 𝑦 = 𝐸 ) ) , 𝑠 / 𝑡 𝐷 ) = if ( 𝑠 ( 𝑝 𝑞 ) , ( 𝑦𝐵𝑡𝐴 ( ( ¬ 𝑡 𝑊 ∧ ¬ 𝑡 ( 𝑝 𝑞 ) ) → 𝑦 = 𝐸 ) ) , 𝑠 / 𝑡 𝐷 )
24 eqid ( 𝑧𝐵𝑠𝐴 ( ( ¬ 𝑠 𝑊 ∧ ( 𝑠 ( 𝑥 𝑊 ) ) = 𝑥 ) → 𝑧 = ( if ( 𝑠 ( 𝑝 𝑞 ) , ( 𝑦𝐵𝑡𝐴 ( ( ¬ 𝑡 𝑊 ∧ ¬ 𝑡 ( 𝑝 𝑞 ) ) → 𝑦 = 𝐸 ) ) , 𝑠 / 𝑡 𝐷 ) ( 𝑥 𝑊 ) ) ) ) = ( 𝑧𝐵𝑠𝐴 ( ( ¬ 𝑠 𝑊 ∧ ( 𝑠 ( 𝑥 𝑊 ) ) = 𝑥 ) → 𝑧 = ( if ( 𝑠 ( 𝑝 𝑞 ) , ( 𝑦𝐵𝑡𝐴 ( ( ¬ 𝑡 𝑊 ∧ ¬ 𝑡 ( 𝑝 𝑞 ) ) → 𝑦 = 𝐸 ) ) , 𝑠 / 𝑡 𝐷 ) ( 𝑥 𝑊 ) ) ) )
25 1 2 3 4 5 6 8 21 9 10 22 23 24 11 12 cdleme42keg ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑝𝐴 ∧ ¬ 𝑝 𝑊 ) ∧ ( 𝑞𝐴 ∧ ¬ 𝑞 𝑊 ) ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ) → ( ( 𝐺𝑃 ) ( 𝐺𝑄 ) ) = ( ( 𝐺𝑃 ) 𝑉 ) )
26 1 2 3 4 5 6 7 8 9 10 11 17 25 cdlemg2ce ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝐹𝑇 ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ) → ( ( 𝐹𝑃 ) ( 𝐹𝑄 ) ) = ( ( 𝐹𝑃 ) 𝑉 ) )
27 26 3com23 ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ 𝐹𝑇 ) → ( ( 𝐹𝑃 ) ( 𝐹𝑄 ) ) = ( ( 𝐹𝑃 ) 𝑉 ) )