Metamath Proof Explorer


Theorem 4atexlemc

Description: Lemma for 4atexlem7 . (Contributed by NM, 24-Nov-2012)

Ref Expression
Hypotheses 4thatlem.ph ( 𝜑 ↔ ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( 𝑆𝐴 ∧ ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ∧ ( 𝑃 𝑅 ) = ( 𝑄 𝑅 ) ) ∧ ( 𝑇𝐴 ∧ ( 𝑈 𝑇 ) = ( 𝑉 𝑇 ) ) ) ∧ ( 𝑃𝑄 ∧ ¬ 𝑆 ( 𝑃 𝑄 ) ) ) )
4thatlem0.l = ( le ‘ 𝐾 )
4thatlem0.j = ( join ‘ 𝐾 )
4thatlem0.m = ( meet ‘ 𝐾 )
4thatlem0.a 𝐴 = ( Atoms ‘ 𝐾 )
4thatlem0.h 𝐻 = ( LHyp ‘ 𝐾 )
4thatlem0.u 𝑈 = ( ( 𝑃 𝑄 ) 𝑊 )
4thatlem0.v 𝑉 = ( ( 𝑃 𝑆 ) 𝑊 )
4thatlem0.c 𝐶 = ( ( 𝑄 𝑇 ) ( 𝑃 𝑆 ) )
Assertion 4atexlemc ( 𝜑𝐶𝐴 )

Proof

Step Hyp Ref Expression
1 4thatlem.ph ( 𝜑 ↔ ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( 𝑆𝐴 ∧ ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ∧ ( 𝑃 𝑅 ) = ( 𝑄 𝑅 ) ) ∧ ( 𝑇𝐴 ∧ ( 𝑈 𝑇 ) = ( 𝑉 𝑇 ) ) ) ∧ ( 𝑃𝑄 ∧ ¬ 𝑆 ( 𝑃 𝑄 ) ) ) )
2 4thatlem0.l = ( le ‘ 𝐾 )
3 4thatlem0.j = ( join ‘ 𝐾 )
4 4thatlem0.m = ( meet ‘ 𝐾 )
5 4thatlem0.a 𝐴 = ( Atoms ‘ 𝐾 )
6 4thatlem0.h 𝐻 = ( LHyp ‘ 𝐾 )
7 4thatlem0.u 𝑈 = ( ( 𝑃 𝑄 ) 𝑊 )
8 4thatlem0.v 𝑉 = ( ( 𝑃 𝑆 ) 𝑊 )
9 4thatlem0.c 𝐶 = ( ( 𝑄 𝑇 ) ( 𝑃 𝑆 ) )
10 1 4atexlemkl ( 𝜑𝐾 ∈ Lat )
11 1 3 5 4atexlemqtb ( 𝜑 → ( 𝑄 𝑇 ) ∈ ( Base ‘ 𝐾 ) )
12 1 3 5 4atexlempsb ( 𝜑 → ( 𝑃 𝑆 ) ∈ ( Base ‘ 𝐾 ) )
13 eqid ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
14 13 4 latmcom ( ( 𝐾 ∈ Lat ∧ ( 𝑄 𝑇 ) ∈ ( Base ‘ 𝐾 ) ∧ ( 𝑃 𝑆 ) ∈ ( Base ‘ 𝐾 ) ) → ( ( 𝑄 𝑇 ) ( 𝑃 𝑆 ) ) = ( ( 𝑃 𝑆 ) ( 𝑄 𝑇 ) ) )
15 10 11 12 14 syl3anc ( 𝜑 → ( ( 𝑄 𝑇 ) ( 𝑃 𝑆 ) ) = ( ( 𝑃 𝑆 ) ( 𝑄 𝑇 ) ) )
16 9 15 syl5eq ( 𝜑𝐶 = ( ( 𝑃 𝑆 ) ( 𝑄 𝑇 ) ) )
17 1 4atexlemk ( 𝜑𝐾 ∈ HL )
18 1 4atexlemp ( 𝜑𝑃𝐴 )
19 1 4atexlems ( 𝜑𝑆𝐴 )
20 1 4atexlemq ( 𝜑𝑄𝐴 )
21 1 4atexlemt ( 𝜑𝑇𝐴 )
22 1 2 3 5 4atexlempns ( 𝜑𝑃𝑆 )
23 1 2 3 4 5 6 7 8 4atexlemntlpq ( 𝜑 → ¬ 𝑇 ( 𝑃 𝑄 ) )
24 2 3 5 atnlej2 ( ( 𝐾 ∈ HL ∧ ( 𝑇𝐴𝑃𝐴𝑄𝐴 ) ∧ ¬ 𝑇 ( 𝑃 𝑄 ) ) → 𝑇𝑄 )
25 24 necomd ( ( 𝐾 ∈ HL ∧ ( 𝑇𝐴𝑃𝐴𝑄𝐴 ) ∧ ¬ 𝑇 ( 𝑃 𝑄 ) ) → 𝑄𝑇 )
26 17 21 18 20 23 25 syl131anc ( 𝜑𝑄𝑇 )
27 1 4atexlempnq ( 𝜑𝑃𝑄 )
28 1 4atexlemnslpq ( 𝜑 → ¬ 𝑆 ( 𝑃 𝑄 ) )
29 2 3 5 4atlem0ae ( ( 𝐾 ∈ HL ∧ ( 𝑃𝐴𝑄𝐴𝑆𝐴 ) ∧ ( 𝑃𝑄 ∧ ¬ 𝑆 ( 𝑃 𝑄 ) ) ) → ¬ 𝑄 ( 𝑃 𝑆 ) )
30 17 18 20 19 27 28 29 syl132anc ( 𝜑 → ¬ 𝑄 ( 𝑃 𝑆 ) )
31 13 5 atbase ( 𝑇𝐴𝑇 ∈ ( Base ‘ 𝐾 ) )
32 21 31 syl ( 𝜑𝑇 ∈ ( Base ‘ 𝐾 ) )
33 1 2 3 4 5 6 7 4atexlemu ( 𝜑𝑈𝐴 )
34 1 2 3 4 5 6 7 8 4atexlemv ( 𝜑𝑉𝐴 )
35 13 3 5 hlatjcl ( ( 𝐾 ∈ HL ∧ 𝑈𝐴𝑉𝐴 ) → ( 𝑈 𝑉 ) ∈ ( Base ‘ 𝐾 ) )
36 17 33 34 35 syl3anc ( 𝜑 → ( 𝑈 𝑉 ) ∈ ( Base ‘ 𝐾 ) )
37 13 5 atbase ( 𝑄𝐴𝑄 ∈ ( Base ‘ 𝐾 ) )
38 20 37 syl ( 𝜑𝑄 ∈ ( Base ‘ 𝐾 ) )
39 13 3 latjcl ( ( 𝐾 ∈ Lat ∧ ( 𝑃 𝑆 ) ∈ ( Base ‘ 𝐾 ) ∧ 𝑄 ∈ ( Base ‘ 𝐾 ) ) → ( ( 𝑃 𝑆 ) 𝑄 ) ∈ ( Base ‘ 𝐾 ) )
40 10 12 38 39 syl3anc ( 𝜑 → ( ( 𝑃 𝑆 ) 𝑄 ) ∈ ( Base ‘ 𝐾 ) )
41 1 4atexlemkc ( 𝜑𝐾 ∈ CvLat )
42 1 2 3 4 5 6 7 8 4atexlemunv ( 𝜑𝑈𝑉 )
43 1 4atexlemutvt ( 𝜑 → ( 𝑈 𝑇 ) = ( 𝑉 𝑇 ) )
44 5 2 3 cvlsupr4 ( ( 𝐾 ∈ CvLat ∧ ( 𝑈𝐴𝑉𝐴𝑇𝐴 ) ∧ ( 𝑈𝑉 ∧ ( 𝑈 𝑇 ) = ( 𝑉 𝑇 ) ) ) → 𝑇 ( 𝑈 𝑉 ) )
45 41 33 34 21 42 43 44 syl132anc ( 𝜑𝑇 ( 𝑈 𝑉 ) )
46 13 3 5 hlatjcl ( ( 𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴 ) → ( 𝑃 𝑄 ) ∈ ( Base ‘ 𝐾 ) )
47 17 18 20 46 syl3anc ( 𝜑 → ( 𝑃 𝑄 ) ∈ ( Base ‘ 𝐾 ) )
48 1 6 4atexlemwb ( 𝜑𝑊 ∈ ( Base ‘ 𝐾 ) )
49 13 2 4 latmle1 ( ( 𝐾 ∈ Lat ∧ ( 𝑃 𝑄 ) ∈ ( Base ‘ 𝐾 ) ∧ 𝑊 ∈ ( Base ‘ 𝐾 ) ) → ( ( 𝑃 𝑄 ) 𝑊 ) ( 𝑃 𝑄 ) )
50 10 47 48 49 syl3anc ( 𝜑 → ( ( 𝑃 𝑄 ) 𝑊 ) ( 𝑃 𝑄 ) )
51 7 50 eqbrtrid ( 𝜑𝑈 ( 𝑃 𝑄 ) )
52 13 2 4 latmle1 ( ( 𝐾 ∈ Lat ∧ ( 𝑃 𝑆 ) ∈ ( Base ‘ 𝐾 ) ∧ 𝑊 ∈ ( Base ‘ 𝐾 ) ) → ( ( 𝑃 𝑆 ) 𝑊 ) ( 𝑃 𝑆 ) )
53 10 12 48 52 syl3anc ( 𝜑 → ( ( 𝑃 𝑆 ) 𝑊 ) ( 𝑃 𝑆 ) )
54 8 53 eqbrtrid ( 𝜑𝑉 ( 𝑃 𝑆 ) )
55 13 5 atbase ( 𝑈𝐴𝑈 ∈ ( Base ‘ 𝐾 ) )
56 33 55 syl ( 𝜑𝑈 ∈ ( Base ‘ 𝐾 ) )
57 13 5 atbase ( 𝑉𝐴𝑉 ∈ ( Base ‘ 𝐾 ) )
58 34 57 syl ( 𝜑𝑉 ∈ ( Base ‘ 𝐾 ) )
59 13 2 3 latjlej12 ( ( 𝐾 ∈ Lat ∧ ( 𝑈 ∈ ( Base ‘ 𝐾 ) ∧ ( 𝑃 𝑄 ) ∈ ( Base ‘ 𝐾 ) ) ∧ ( 𝑉 ∈ ( Base ‘ 𝐾 ) ∧ ( 𝑃 𝑆 ) ∈ ( Base ‘ 𝐾 ) ) ) → ( ( 𝑈 ( 𝑃 𝑄 ) ∧ 𝑉 ( 𝑃 𝑆 ) ) → ( 𝑈 𝑉 ) ( ( 𝑃 𝑄 ) ( 𝑃 𝑆 ) ) ) )
60 10 56 47 58 12 59 syl122anc ( 𝜑 → ( ( 𝑈 ( 𝑃 𝑄 ) ∧ 𝑉 ( 𝑃 𝑆 ) ) → ( 𝑈 𝑉 ) ( ( 𝑃 𝑄 ) ( 𝑃 𝑆 ) ) ) )
61 51 54 60 mp2and ( 𝜑 → ( 𝑈 𝑉 ) ( ( 𝑃 𝑄 ) ( 𝑃 𝑆 ) ) )
62 3 5 hlatjass ( ( 𝐾 ∈ HL ∧ ( 𝑃𝐴𝑄𝐴𝑆𝐴 ) ) → ( ( 𝑃 𝑄 ) 𝑆 ) = ( 𝑃 ( 𝑄 𝑆 ) ) )
63 17 18 20 19 62 syl13anc ( 𝜑 → ( ( 𝑃 𝑄 ) 𝑆 ) = ( 𝑃 ( 𝑄 𝑆 ) ) )
64 13 5 atbase ( 𝑃𝐴𝑃 ∈ ( Base ‘ 𝐾 ) )
65 18 64 syl ( 𝜑𝑃 ∈ ( Base ‘ 𝐾 ) )
66 13 5 atbase ( 𝑆𝐴𝑆 ∈ ( Base ‘ 𝐾 ) )
67 19 66 syl ( 𝜑𝑆 ∈ ( Base ‘ 𝐾 ) )
68 13 3 latj32 ( ( 𝐾 ∈ Lat ∧ ( 𝑃 ∈ ( Base ‘ 𝐾 ) ∧ 𝑄 ∈ ( Base ‘ 𝐾 ) ∧ 𝑆 ∈ ( Base ‘ 𝐾 ) ) ) → ( ( 𝑃 𝑄 ) 𝑆 ) = ( ( 𝑃 𝑆 ) 𝑄 ) )
69 10 65 38 67 68 syl13anc ( 𝜑 → ( ( 𝑃 𝑄 ) 𝑆 ) = ( ( 𝑃 𝑆 ) 𝑄 ) )
70 13 3 latjjdi ( ( 𝐾 ∈ Lat ∧ ( 𝑃 ∈ ( Base ‘ 𝐾 ) ∧ 𝑄 ∈ ( Base ‘ 𝐾 ) ∧ 𝑆 ∈ ( Base ‘ 𝐾 ) ) ) → ( 𝑃 ( 𝑄 𝑆 ) ) = ( ( 𝑃 𝑄 ) ( 𝑃 𝑆 ) ) )
71 10 65 38 67 70 syl13anc ( 𝜑 → ( 𝑃 ( 𝑄 𝑆 ) ) = ( ( 𝑃 𝑄 ) ( 𝑃 𝑆 ) ) )
72 63 69 71 3eqtr3rd ( 𝜑 → ( ( 𝑃 𝑄 ) ( 𝑃 𝑆 ) ) = ( ( 𝑃 𝑆 ) 𝑄 ) )
73 61 72 breqtrd ( 𝜑 → ( 𝑈 𝑉 ) ( ( 𝑃 𝑆 ) 𝑄 ) )
74 13 2 10 32 36 40 45 73 lattrd ( 𝜑𝑇 ( ( 𝑃 𝑆 ) 𝑄 ) )
75 2 3 4 5 2atmat ( ( ( 𝐾 ∈ HL ∧ 𝑃𝐴𝑆𝐴 ) ∧ ( 𝑄𝐴𝑇𝐴𝑃𝑆 ) ∧ ( 𝑄𝑇 ∧ ¬ 𝑄 ( 𝑃 𝑆 ) ∧ 𝑇 ( ( 𝑃 𝑆 ) 𝑄 ) ) ) → ( ( 𝑃 𝑆 ) ( 𝑄 𝑇 ) ) ∈ 𝐴 )
76 17 18 19 20 21 22 26 30 74 75 syl333anc ( 𝜑 → ( ( 𝑃 𝑆 ) ( 𝑄 𝑇 ) ) ∈ 𝐴 )
77 16 76 eqeltrd ( 𝜑𝐶𝐴 )