Metamath Proof Explorer


Theorem cdleme20aN

Description: Part of proof of Lemma E in Crawley p. 113, last paragraph on p. 114. D , F , Y , G represent s_2, f(s), t_2, f(t). (Contributed by NM, 14-Nov-2012) (New usage is discouraged.)

Ref Expression
Hypotheses cdleme19.l = ( le ‘ 𝐾 )
cdleme19.j = ( join ‘ 𝐾 )
cdleme19.m = ( meet ‘ 𝐾 )
cdleme19.a 𝐴 = ( Atoms ‘ 𝐾 )
cdleme19.h 𝐻 = ( LHyp ‘ 𝐾 )
cdleme19.u 𝑈 = ( ( 𝑃 𝑄 ) 𝑊 )
cdleme19.f 𝐹 = ( ( 𝑆 𝑈 ) ( 𝑄 ( ( 𝑃 𝑆 ) 𝑊 ) ) )
cdleme19.g 𝐺 = ( ( 𝑇 𝑈 ) ( 𝑄 ( ( 𝑃 𝑇 ) 𝑊 ) ) )
cdleme19.d 𝐷 = ( ( 𝑅 𝑆 ) 𝑊 )
cdleme19.y 𝑌 = ( ( 𝑅 𝑇 ) 𝑊 )
cdleme20.v 𝑉 = ( ( 𝑆 𝑇 ) 𝑊 )
Assertion cdleme20aN ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑅𝐴𝑆𝐴 ∧ ¬ 𝑆 𝑊 ) ∧ ( 𝑇𝐴 ∧ ¬ 𝑆 ( 𝑃 𝑄 ) ∧ 𝑅 ( 𝑃 𝑄 ) ) ) → ( 𝑉 𝐷 ) = ( ( ( 𝑆 𝑅 ) 𝑇 ) 𝑊 ) )

Proof

Step Hyp Ref Expression
1 cdleme19.l = ( le ‘ 𝐾 )
2 cdleme19.j = ( join ‘ 𝐾 )
3 cdleme19.m = ( meet ‘ 𝐾 )
4 cdleme19.a 𝐴 = ( Atoms ‘ 𝐾 )
5 cdleme19.h 𝐻 = ( LHyp ‘ 𝐾 )
6 cdleme19.u 𝑈 = ( ( 𝑃 𝑄 ) 𝑊 )
7 cdleme19.f 𝐹 = ( ( 𝑆 𝑈 ) ( 𝑄 ( ( 𝑃 𝑆 ) 𝑊 ) ) )
8 cdleme19.g 𝐺 = ( ( 𝑇 𝑈 ) ( 𝑄 ( ( 𝑃 𝑇 ) 𝑊 ) ) )
9 cdleme19.d 𝐷 = ( ( 𝑅 𝑆 ) 𝑊 )
10 cdleme19.y 𝑌 = ( ( 𝑅 𝑇 ) 𝑊 )
11 cdleme20.v 𝑉 = ( ( 𝑆 𝑇 ) 𝑊 )
12 11 oveq1i ( 𝑉 𝐷 ) = ( ( ( 𝑆 𝑇 ) 𝑊 ) 𝐷 )
13 simp1l ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑅𝐴𝑆𝐴 ∧ ¬ 𝑆 𝑊 ) ∧ ( 𝑇𝐴 ∧ ¬ 𝑆 ( 𝑃 𝑄 ) ∧ 𝑅 ( 𝑃 𝑄 ) ) ) → 𝐾 ∈ HL )
14 simp1r ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑅𝐴𝑆𝐴 ∧ ¬ 𝑆 𝑊 ) ∧ ( 𝑇𝐴 ∧ ¬ 𝑆 ( 𝑃 𝑄 ) ∧ 𝑅 ( 𝑃 𝑄 ) ) ) → 𝑊𝐻 )
15 simp22 ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑅𝐴𝑆𝐴 ∧ ¬ 𝑆 𝑊 ) ∧ ( 𝑇𝐴 ∧ ¬ 𝑆 ( 𝑃 𝑄 ) ∧ 𝑅 ( 𝑃 𝑄 ) ) ) → 𝑆𝐴 )
16 simp23 ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑅𝐴𝑆𝐴 ∧ ¬ 𝑆 𝑊 ) ∧ ( 𝑇𝐴 ∧ ¬ 𝑆 ( 𝑃 𝑄 ) ∧ 𝑅 ( 𝑃 𝑄 ) ) ) → ¬ 𝑆 𝑊 )
17 simp21 ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑅𝐴𝑆𝐴 ∧ ¬ 𝑆 𝑊 ) ∧ ( 𝑇𝐴 ∧ ¬ 𝑆 ( 𝑃 𝑄 ) ∧ 𝑅 ( 𝑃 𝑄 ) ) ) → 𝑅𝐴 )
18 simp33 ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑅𝐴𝑆𝐴 ∧ ¬ 𝑆 𝑊 ) ∧ ( 𝑇𝐴 ∧ ¬ 𝑆 ( 𝑃 𝑄 ) ∧ 𝑅 ( 𝑃 𝑄 ) ) ) → 𝑅 ( 𝑃 𝑄 ) )
19 simp32 ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑅𝐴𝑆𝐴 ∧ ¬ 𝑆 𝑊 ) ∧ ( 𝑇𝐴 ∧ ¬ 𝑆 ( 𝑃 𝑄 ) ∧ 𝑅 ( 𝑃 𝑄 ) ) ) → ¬ 𝑆 ( 𝑃 𝑄 ) )
20 1 2 3 4 5 9 cdlemeda ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑆𝐴 ∧ ¬ 𝑆 𝑊 ) ∧ ( 𝑅𝐴𝑅 ( 𝑃 𝑄 ) ∧ ¬ 𝑆 ( 𝑃 𝑄 ) ) ) → 𝐷𝐴 )
21 13 14 15 16 17 18 19 20 syl223anc ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑅𝐴𝑆𝐴 ∧ ¬ 𝑆 𝑊 ) ∧ ( 𝑇𝐴 ∧ ¬ 𝑆 ( 𝑃 𝑄 ) ∧ 𝑅 ( 𝑃 𝑄 ) ) ) → 𝐷𝐴 )
22 simp31 ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑅𝐴𝑆𝐴 ∧ ¬ 𝑆 𝑊 ) ∧ ( 𝑇𝐴 ∧ ¬ 𝑆 ( 𝑃 𝑄 ) ∧ 𝑅 ( 𝑃 𝑄 ) ) ) → 𝑇𝐴 )
23 eqid ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
24 23 2 4 hlatjcl ( ( 𝐾 ∈ HL ∧ 𝑆𝐴𝑇𝐴 ) → ( 𝑆 𝑇 ) ∈ ( Base ‘ 𝐾 ) )
25 13 15 22 24 syl3anc ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑅𝐴𝑆𝐴 ∧ ¬ 𝑆 𝑊 ) ∧ ( 𝑇𝐴 ∧ ¬ 𝑆 ( 𝑃 𝑄 ) ∧ 𝑅 ( 𝑃 𝑄 ) ) ) → ( 𝑆 𝑇 ) ∈ ( Base ‘ 𝐾 ) )
26 23 5 lhpbase ( 𝑊𝐻𝑊 ∈ ( Base ‘ 𝐾 ) )
27 14 26 syl ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑅𝐴𝑆𝐴 ∧ ¬ 𝑆 𝑊 ) ∧ ( 𝑇𝐴 ∧ ¬ 𝑆 ( 𝑃 𝑄 ) ∧ 𝑅 ( 𝑃 𝑄 ) ) ) → 𝑊 ∈ ( Base ‘ 𝐾 ) )
28 13 hllatd ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑅𝐴𝑆𝐴 ∧ ¬ 𝑆 𝑊 ) ∧ ( 𝑇𝐴 ∧ ¬ 𝑆 ( 𝑃 𝑄 ) ∧ 𝑅 ( 𝑃 𝑄 ) ) ) → 𝐾 ∈ Lat )
29 23 2 4 hlatjcl ( ( 𝐾 ∈ HL ∧ 𝑅𝐴𝑆𝐴 ) → ( 𝑅 𝑆 ) ∈ ( Base ‘ 𝐾 ) )
30 13 17 15 29 syl3anc ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑅𝐴𝑆𝐴 ∧ ¬ 𝑆 𝑊 ) ∧ ( 𝑇𝐴 ∧ ¬ 𝑆 ( 𝑃 𝑄 ) ∧ 𝑅 ( 𝑃 𝑄 ) ) ) → ( 𝑅 𝑆 ) ∈ ( Base ‘ 𝐾 ) )
31 23 1 3 latmle2 ( ( 𝐾 ∈ Lat ∧ ( 𝑅 𝑆 ) ∈ ( Base ‘ 𝐾 ) ∧ 𝑊 ∈ ( Base ‘ 𝐾 ) ) → ( ( 𝑅 𝑆 ) 𝑊 ) 𝑊 )
32 28 30 27 31 syl3anc ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑅𝐴𝑆𝐴 ∧ ¬ 𝑆 𝑊 ) ∧ ( 𝑇𝐴 ∧ ¬ 𝑆 ( 𝑃 𝑄 ) ∧ 𝑅 ( 𝑃 𝑄 ) ) ) → ( ( 𝑅 𝑆 ) 𝑊 ) 𝑊 )
33 9 32 eqbrtrid ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑅𝐴𝑆𝐴 ∧ ¬ 𝑆 𝑊 ) ∧ ( 𝑇𝐴 ∧ ¬ 𝑆 ( 𝑃 𝑄 ) ∧ 𝑅 ( 𝑃 𝑄 ) ) ) → 𝐷 𝑊 )
34 23 1 2 3 4 atmod4i1 ( ( 𝐾 ∈ HL ∧ ( 𝐷𝐴 ∧ ( 𝑆 𝑇 ) ∈ ( Base ‘ 𝐾 ) ∧ 𝑊 ∈ ( Base ‘ 𝐾 ) ) ∧ 𝐷 𝑊 ) → ( ( ( 𝑆 𝑇 ) 𝑊 ) 𝐷 ) = ( ( ( 𝑆 𝑇 ) 𝐷 ) 𝑊 ) )
35 13 21 25 27 33 34 syl131anc ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑅𝐴𝑆𝐴 ∧ ¬ 𝑆 𝑊 ) ∧ ( 𝑇𝐴 ∧ ¬ 𝑆 ( 𝑃 𝑄 ) ∧ 𝑅 ( 𝑃 𝑄 ) ) ) → ( ( ( 𝑆 𝑇 ) 𝑊 ) 𝐷 ) = ( ( ( 𝑆 𝑇 ) 𝐷 ) 𝑊 ) )
36 1 2 3 4 5 9 cdleme10 ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝑅𝐴 ∧ ( 𝑆𝐴 ∧ ¬ 𝑆 𝑊 ) ) → ( 𝑆 𝐷 ) = ( 𝑆 𝑅 ) )
37 13 14 17 15 16 36 syl212anc ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑅𝐴𝑆𝐴 ∧ ¬ 𝑆 𝑊 ) ∧ ( 𝑇𝐴 ∧ ¬ 𝑆 ( 𝑃 𝑄 ) ∧ 𝑅 ( 𝑃 𝑄 ) ) ) → ( 𝑆 𝐷 ) = ( 𝑆 𝑅 ) )
38 37 oveq1d ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑅𝐴𝑆𝐴 ∧ ¬ 𝑆 𝑊 ) ∧ ( 𝑇𝐴 ∧ ¬ 𝑆 ( 𝑃 𝑄 ) ∧ 𝑅 ( 𝑃 𝑄 ) ) ) → ( ( 𝑆 𝐷 ) 𝑇 ) = ( ( 𝑆 𝑅 ) 𝑇 ) )
39 2 4 hlatj32 ( ( 𝐾 ∈ HL ∧ ( 𝑆𝐴𝐷𝐴𝑇𝐴 ) ) → ( ( 𝑆 𝐷 ) 𝑇 ) = ( ( 𝑆 𝑇 ) 𝐷 ) )
40 13 15 21 22 39 syl13anc ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑅𝐴𝑆𝐴 ∧ ¬ 𝑆 𝑊 ) ∧ ( 𝑇𝐴 ∧ ¬ 𝑆 ( 𝑃 𝑄 ) ∧ 𝑅 ( 𝑃 𝑄 ) ) ) → ( ( 𝑆 𝐷 ) 𝑇 ) = ( ( 𝑆 𝑇 ) 𝐷 ) )
41 38 40 eqtr3d ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑅𝐴𝑆𝐴 ∧ ¬ 𝑆 𝑊 ) ∧ ( 𝑇𝐴 ∧ ¬ 𝑆 ( 𝑃 𝑄 ) ∧ 𝑅 ( 𝑃 𝑄 ) ) ) → ( ( 𝑆 𝑅 ) 𝑇 ) = ( ( 𝑆 𝑇 ) 𝐷 ) )
42 41 oveq1d ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑅𝐴𝑆𝐴 ∧ ¬ 𝑆 𝑊 ) ∧ ( 𝑇𝐴 ∧ ¬ 𝑆 ( 𝑃 𝑄 ) ∧ 𝑅 ( 𝑃 𝑄 ) ) ) → ( ( ( 𝑆 𝑅 ) 𝑇 ) 𝑊 ) = ( ( ( 𝑆 𝑇 ) 𝐷 ) 𝑊 ) )
43 35 42 eqtr4d ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑅𝐴𝑆𝐴 ∧ ¬ 𝑆 𝑊 ) ∧ ( 𝑇𝐴 ∧ ¬ 𝑆 ( 𝑃 𝑄 ) ∧ 𝑅 ( 𝑃 𝑄 ) ) ) → ( ( ( 𝑆 𝑇 ) 𝑊 ) 𝐷 ) = ( ( ( 𝑆 𝑅 ) 𝑇 ) 𝑊 ) )
44 12 43 syl5eq ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑅𝐴𝑆𝐴 ∧ ¬ 𝑆 𝑊 ) ∧ ( 𝑇𝐴 ∧ ¬ 𝑆 ( 𝑃 𝑄 ) ∧ 𝑅 ( 𝑃 𝑄 ) ) ) → ( 𝑉 𝐷 ) = ( ( ( 𝑆 𝑅 ) 𝑇 ) 𝑊 ) )