Metamath Proof Explorer


Theorem cdlemd1

Description: Part of proof of Lemma D in Crawley p. 113. (Contributed by NM, 29-May-2012)

Ref Expression
Hypotheses cdlemd1.l = ( le ‘ 𝐾 )
cdlemd1.j = ( join ‘ 𝐾 )
cdlemd1.m = ( meet ‘ 𝐾 )
cdlemd1.a 𝐴 = ( Atoms ‘ 𝐾 )
cdlemd1.h 𝐻 = ( LHyp ‘ 𝐾 )
Assertion cdlemd1 ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ ( 𝑅𝐴𝑃𝑄 ∧ ¬ 𝑅 ( 𝑃 𝑄 ) ) ) ) → 𝑅 = ( ( 𝑃 ( ( 𝑃 𝑅 ) 𝑊 ) ) ( 𝑄 ( ( 𝑄 𝑅 ) 𝑊 ) ) ) )

Proof

Step Hyp Ref Expression
1 cdlemd1.l = ( le ‘ 𝐾 )
2 cdlemd1.j = ( join ‘ 𝐾 )
3 cdlemd1.m = ( meet ‘ 𝐾 )
4 cdlemd1.a 𝐴 = ( Atoms ‘ 𝐾 )
5 cdlemd1.h 𝐻 = ( LHyp ‘ 𝐾 )
6 simpll ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ ( 𝑅𝐴𝑃𝑄 ∧ ¬ 𝑅 ( 𝑃 𝑄 ) ) ) ) → 𝐾 ∈ HL )
7 simpr1l ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ ( 𝑅𝐴𝑃𝑄 ∧ ¬ 𝑅 ( 𝑃 𝑄 ) ) ) ) → 𝑃𝐴 )
8 simpr2l ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ ( 𝑅𝐴𝑃𝑄 ∧ ¬ 𝑅 ( 𝑃 𝑄 ) ) ) ) → 𝑄𝐴 )
9 simpr31 ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ ( 𝑅𝐴𝑃𝑄 ∧ ¬ 𝑅 ( 𝑃 𝑄 ) ) ) ) → 𝑅𝐴 )
10 simpr32 ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ ( 𝑅𝐴𝑃𝑄 ∧ ¬ 𝑅 ( 𝑃 𝑄 ) ) ) ) → 𝑃𝑄 )
11 simpr33 ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ ( 𝑅𝐴𝑃𝑄 ∧ ¬ 𝑅 ( 𝑃 𝑄 ) ) ) ) → ¬ 𝑅 ( 𝑃 𝑄 ) )
12 1 2 3 4 2llnma2 ( ( 𝐾 ∈ HL ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ∧ ( 𝑃𝑄 ∧ ¬ 𝑅 ( 𝑃 𝑄 ) ) ) → ( ( 𝑅 𝑃 ) ( 𝑅 𝑄 ) ) = 𝑅 )
13 6 7 8 9 10 11 12 syl132anc ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ ( 𝑅𝐴𝑃𝑄 ∧ ¬ 𝑅 ( 𝑃 𝑄 ) ) ) ) → ( ( 𝑅 𝑃 ) ( 𝑅 𝑄 ) ) = 𝑅 )
14 hllat ( 𝐾 ∈ HL → 𝐾 ∈ Lat )
15 14 ad2antrr ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ ( 𝑅𝐴𝑃𝑄 ∧ ¬ 𝑅 ( 𝑃 𝑄 ) ) ) ) → 𝐾 ∈ Lat )
16 eqid ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
17 16 4 atbase ( 𝑅𝐴𝑅 ∈ ( Base ‘ 𝐾 ) )
18 9 17 syl ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ ( 𝑅𝐴𝑃𝑄 ∧ ¬ 𝑅 ( 𝑃 𝑄 ) ) ) ) → 𝑅 ∈ ( Base ‘ 𝐾 ) )
19 16 4 atbase ( 𝑃𝐴𝑃 ∈ ( Base ‘ 𝐾 ) )
20 7 19 syl ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ ( 𝑅𝐴𝑃𝑄 ∧ ¬ 𝑅 ( 𝑃 𝑄 ) ) ) ) → 𝑃 ∈ ( Base ‘ 𝐾 ) )
21 16 2 latjcom ( ( 𝐾 ∈ Lat ∧ 𝑅 ∈ ( Base ‘ 𝐾 ) ∧ 𝑃 ∈ ( Base ‘ 𝐾 ) ) → ( 𝑅 𝑃 ) = ( 𝑃 𝑅 ) )
22 15 18 20 21 syl3anc ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ ( 𝑅𝐴𝑃𝑄 ∧ ¬ 𝑅 ( 𝑃 𝑄 ) ) ) ) → ( 𝑅 𝑃 ) = ( 𝑃 𝑅 ) )
23 simpl ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ ( 𝑅𝐴𝑃𝑄 ∧ ¬ 𝑅 ( 𝑃 𝑄 ) ) ) ) → ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) )
24 simpr1 ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ ( 𝑅𝐴𝑃𝑄 ∧ ¬ 𝑅 ( 𝑃 𝑄 ) ) ) ) → ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) )
25 16 1 2 3 4 5 cdlemc1 ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝑅 ∈ ( Base ‘ 𝐾 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ) → ( 𝑃 ( ( 𝑃 𝑅 ) 𝑊 ) ) = ( 𝑃 𝑅 ) )
26 23 18 24 25 syl3anc ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ ( 𝑅𝐴𝑃𝑄 ∧ ¬ 𝑅 ( 𝑃 𝑄 ) ) ) ) → ( 𝑃 ( ( 𝑃 𝑅 ) 𝑊 ) ) = ( 𝑃 𝑅 ) )
27 22 26 eqtr4d ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ ( 𝑅𝐴𝑃𝑄 ∧ ¬ 𝑅 ( 𝑃 𝑄 ) ) ) ) → ( 𝑅 𝑃 ) = ( 𝑃 ( ( 𝑃 𝑅 ) 𝑊 ) ) )
28 16 4 atbase ( 𝑄𝐴𝑄 ∈ ( Base ‘ 𝐾 ) )
29 8 28 syl ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ ( 𝑅𝐴𝑃𝑄 ∧ ¬ 𝑅 ( 𝑃 𝑄 ) ) ) ) → 𝑄 ∈ ( Base ‘ 𝐾 ) )
30 16 2 latjcom ( ( 𝐾 ∈ Lat ∧ 𝑅 ∈ ( Base ‘ 𝐾 ) ∧ 𝑄 ∈ ( Base ‘ 𝐾 ) ) → ( 𝑅 𝑄 ) = ( 𝑄 𝑅 ) )
31 15 18 29 30 syl3anc ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ ( 𝑅𝐴𝑃𝑄 ∧ ¬ 𝑅 ( 𝑃 𝑄 ) ) ) ) → ( 𝑅 𝑄 ) = ( 𝑄 𝑅 ) )
32 simpr2 ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ ( 𝑅𝐴𝑃𝑄 ∧ ¬ 𝑅 ( 𝑃 𝑄 ) ) ) ) → ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) )
33 16 1 2 3 4 5 cdlemc1 ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝑅 ∈ ( Base ‘ 𝐾 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) → ( 𝑄 ( ( 𝑄 𝑅 ) 𝑊 ) ) = ( 𝑄 𝑅 ) )
34 23 18 32 33 syl3anc ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ ( 𝑅𝐴𝑃𝑄 ∧ ¬ 𝑅 ( 𝑃 𝑄 ) ) ) ) → ( 𝑄 ( ( 𝑄 𝑅 ) 𝑊 ) ) = ( 𝑄 𝑅 ) )
35 31 34 eqtr4d ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ ( 𝑅𝐴𝑃𝑄 ∧ ¬ 𝑅 ( 𝑃 𝑄 ) ) ) ) → ( 𝑅 𝑄 ) = ( 𝑄 ( ( 𝑄 𝑅 ) 𝑊 ) ) )
36 27 35 oveq12d ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ ( 𝑅𝐴𝑃𝑄 ∧ ¬ 𝑅 ( 𝑃 𝑄 ) ) ) ) → ( ( 𝑅 𝑃 ) ( 𝑅 𝑄 ) ) = ( ( 𝑃 ( ( 𝑃 𝑅 ) 𝑊 ) ) ( 𝑄 ( ( 𝑄 𝑅 ) 𝑊 ) ) ) )
37 13 36 eqtr3d ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ ( 𝑅𝐴𝑃𝑄 ∧ ¬ 𝑅 ( 𝑃 𝑄 ) ) ) ) → 𝑅 = ( ( 𝑃 ( ( 𝑃 𝑅 ) 𝑊 ) ) ( 𝑄 ( ( 𝑄 𝑅 ) 𝑊 ) ) ) )