Metamath Proof Explorer


Theorem 4atlem12a

Description: Lemma for 4at . Substitute T for P . (Contributed by NM, 9-Jul-2012)

Ref Expression
Hypotheses 4at.l ˙=K
4at.j ˙=joinK
4at.a A=AtomsK
Assertion 4atlem12a KHLPATAUAVAWA¬P˙U˙V˙WP˙T˙U˙V˙WP˙U˙V˙W=T˙U˙V˙W

Proof

Step Hyp Ref Expression
1 4at.l ˙=K
2 4at.j ˙=joinK
3 4at.a A=AtomsK
4 simp11 KHLPATAUAVAWA¬P˙U˙V˙WKHL
5 simp12 KHLPATAUAVAWA¬P˙U˙V˙WPA
6 simp13 KHLPATAUAVAWA¬P˙U˙V˙WTA
7 4 hllatd KHLPATAUAVAWA¬P˙U˙V˙WKLat
8 simp21 KHLPATAUAVAWA¬P˙U˙V˙WUA
9 simp22 KHLPATAUAVAWA¬P˙U˙V˙WVA
10 eqid BaseK=BaseK
11 10 2 3 hlatjcl KHLUAVAU˙VBaseK
12 4 8 9 11 syl3anc KHLPATAUAVAWA¬P˙U˙V˙WU˙VBaseK
13 simp23 KHLPATAUAVAWA¬P˙U˙V˙WWA
14 10 3 atbase WAWBaseK
15 13 14 syl KHLPATAUAVAWA¬P˙U˙V˙WWBaseK
16 10 2 latjcl KLatU˙VBaseKWBaseKU˙V˙WBaseK
17 7 12 15 16 syl3anc KHLPATAUAVAWA¬P˙U˙V˙WU˙V˙WBaseK
18 simp3 KHLPATAUAVAWA¬P˙U˙V˙W¬P˙U˙V˙W
19 10 1 2 3 hlexchb2 KHLPATAU˙V˙WBaseK¬P˙U˙V˙WP˙T˙U˙V˙WP˙U˙V˙W=T˙U˙V˙W
20 4 5 6 17 18 19 syl131anc KHLPATAUAVAWA¬P˙U˙V˙WP˙T˙U˙V˙WP˙U˙V˙W=T˙U˙V˙W
21 1 2 3 4atlem4a KHLTAUAVAWAT˙U˙V˙W=T˙U˙V˙W
22 4 6 8 9 13 21 syl32anc KHLPATAUAVAWA¬P˙U˙V˙WT˙U˙V˙W=T˙U˙V˙W
23 22 breq2d KHLPATAUAVAWA¬P˙U˙V˙WP˙T˙U˙V˙WP˙T˙U˙V˙W
24 1 2 3 4atlem4a KHLPAUAVAWAP˙U˙V˙W=P˙U˙V˙W
25 4 5 8 9 13 24 syl32anc KHLPATAUAVAWA¬P˙U˙V˙WP˙U˙V˙W=P˙U˙V˙W
26 25 22 eqeq12d KHLPATAUAVAWA¬P˙U˙V˙WP˙U˙V˙W=T˙U˙V˙WP˙U˙V˙W=T˙U˙V˙W
27 20 23 26 3bitr4d KHLPATAUAVAWA¬P˙U˙V˙WP˙T˙U˙V˙WP˙U˙V˙W=T˙U˙V˙W