Metamath Proof Explorer


Theorem dalawlem1

Description: Lemma for dalaw . Special case of dath2 , where C is replaced by ( ( P .\/ S ) ./\ ( Q .\/ T ) ) . The remaining lemmas will eliminate the conditions on the atoms imposed by dath2 . (Contributed by NM, 6-Oct-2012)

Ref Expression
Hypotheses dalawlem.l ˙=K
dalawlem.j ˙=joinK
dalawlem.m ˙=meetK
dalawlem.a A=AtomsK
dalawlem.o O=LPlanesK
Assertion dalawlem1 KHLPAQARASATAUAP˙Q˙ROS˙T˙UO¬P˙S˙Q˙T˙P˙Q¬P˙S˙Q˙T˙Q˙R¬P˙S˙Q˙T˙R˙P¬P˙S˙Q˙T˙S˙T¬P˙S˙Q˙T˙T˙U¬P˙S˙Q˙T˙U˙SP˙S˙Q˙T˙R˙UP˙Q˙S˙T˙Q˙R˙T˙U˙R˙P˙U˙S

Proof

Step Hyp Ref Expression
1 dalawlem.l ˙=K
2 dalawlem.j ˙=joinK
3 dalawlem.m ˙=meetK
4 dalawlem.a A=AtomsK
5 dalawlem.o O=LPlanesK
6 simp11 KHLPAQARASATAUAP˙Q˙ROS˙T˙UO¬P˙S˙Q˙T˙P˙Q¬P˙S˙Q˙T˙Q˙R¬P˙S˙Q˙T˙R˙P¬P˙S˙Q˙T˙S˙T¬P˙S˙Q˙T˙T˙U¬P˙S˙Q˙T˙U˙SP˙S˙Q˙T˙R˙UKHL
7 6 hllatd KHLPAQARASATAUAP˙Q˙ROS˙T˙UO¬P˙S˙Q˙T˙P˙Q¬P˙S˙Q˙T˙Q˙R¬P˙S˙Q˙T˙R˙P¬P˙S˙Q˙T˙S˙T¬P˙S˙Q˙T˙T˙U¬P˙S˙Q˙T˙U˙SP˙S˙Q˙T˙R˙UKLat
8 simp121 KHLPAQARASATAUAP˙Q˙ROS˙T˙UO¬P˙S˙Q˙T˙P˙Q¬P˙S˙Q˙T˙Q˙R¬P˙S˙Q˙T˙R˙P¬P˙S˙Q˙T˙S˙T¬P˙S˙Q˙T˙T˙U¬P˙S˙Q˙T˙U˙SP˙S˙Q˙T˙R˙UPA
9 simp131 KHLPAQARASATAUAP˙Q˙ROS˙T˙UO¬P˙S˙Q˙T˙P˙Q¬P˙S˙Q˙T˙Q˙R¬P˙S˙Q˙T˙R˙P¬P˙S˙Q˙T˙S˙T¬P˙S˙Q˙T˙T˙U¬P˙S˙Q˙T˙U˙SP˙S˙Q˙T˙R˙USA
10 eqid BaseK=BaseK
11 10 2 4 hlatjcl KHLPASAP˙SBaseK
12 6 8 9 11 syl3anc KHLPAQARASATAUAP˙Q˙ROS˙T˙UO¬P˙S˙Q˙T˙P˙Q¬P˙S˙Q˙T˙Q˙R¬P˙S˙Q˙T˙R˙P¬P˙S˙Q˙T˙S˙T¬P˙S˙Q˙T˙T˙U¬P˙S˙Q˙T˙U˙SP˙S˙Q˙T˙R˙UP˙SBaseK
13 simp122 KHLPAQARASATAUAP˙Q˙ROS˙T˙UO¬P˙S˙Q˙T˙P˙Q¬P˙S˙Q˙T˙Q˙R¬P˙S˙Q˙T˙R˙P¬P˙S˙Q˙T˙S˙T¬P˙S˙Q˙T˙T˙U¬P˙S˙Q˙T˙U˙SP˙S˙Q˙T˙R˙UQA
14 simp132 KHLPAQARASATAUAP˙Q˙ROS˙T˙UO¬P˙S˙Q˙T˙P˙Q¬P˙S˙Q˙T˙Q˙R¬P˙S˙Q˙T˙R˙P¬P˙S˙Q˙T˙S˙T¬P˙S˙Q˙T˙T˙U¬P˙S˙Q˙T˙U˙SP˙S˙Q˙T˙R˙UTA
15 10 2 4 hlatjcl KHLQATAQ˙TBaseK
16 6 13 14 15 syl3anc KHLPAQARASATAUAP˙Q˙ROS˙T˙UO¬P˙S˙Q˙T˙P˙Q¬P˙S˙Q˙T˙Q˙R¬P˙S˙Q˙T˙R˙P¬P˙S˙Q˙T˙S˙T¬P˙S˙Q˙T˙T˙U¬P˙S˙Q˙T˙U˙SP˙S˙Q˙T˙R˙UQ˙TBaseK
17 10 3 latmcl KLatP˙SBaseKQ˙TBaseKP˙S˙Q˙TBaseK
18 7 12 16 17 syl3anc KHLPAQARASATAUAP˙Q˙ROS˙T˙UO¬P˙S˙Q˙T˙P˙Q¬P˙S˙Q˙T˙Q˙R¬P˙S˙Q˙T˙R˙P¬P˙S˙Q˙T˙S˙T¬P˙S˙Q˙T˙T˙U¬P˙S˙Q˙T˙U˙SP˙S˙Q˙T˙R˙UP˙S˙Q˙TBaseK
19 6 18 jca KHLPAQARASATAUAP˙Q˙ROS˙T˙UO¬P˙S˙Q˙T˙P˙Q¬P˙S˙Q˙T˙Q˙R¬P˙S˙Q˙T˙R˙P¬P˙S˙Q˙T˙S˙T¬P˙S˙Q˙T˙T˙U¬P˙S˙Q˙T˙U˙SP˙S˙Q˙T˙R˙UKHLP˙S˙Q˙TBaseK
20 simp12 KHLPAQARASATAUAP˙Q˙ROS˙T˙UO¬P˙S˙Q˙T˙P˙Q¬P˙S˙Q˙T˙Q˙R¬P˙S˙Q˙T˙R˙P¬P˙S˙Q˙T˙S˙T¬P˙S˙Q˙T˙T˙U¬P˙S˙Q˙T˙U˙SP˙S˙Q˙T˙R˙UPAQARA
21 simp13 KHLPAQARASATAUAP˙Q˙ROS˙T˙UO¬P˙S˙Q˙T˙P˙Q¬P˙S˙Q˙T˙Q˙R¬P˙S˙Q˙T˙R˙P¬P˙S˙Q˙T˙S˙T¬P˙S˙Q˙T˙T˙U¬P˙S˙Q˙T˙U˙SP˙S˙Q˙T˙R˙USATAUA
22 simp2l KHLPAQARASATAUAP˙Q˙ROS˙T˙UO¬P˙S˙Q˙T˙P˙Q¬P˙S˙Q˙T˙Q˙R¬P˙S˙Q˙T˙R˙P¬P˙S˙Q˙T˙S˙T¬P˙S˙Q˙T˙T˙U¬P˙S˙Q˙T˙U˙SP˙S˙Q˙T˙R˙UP˙Q˙RO
23 simp2r KHLPAQARASATAUAP˙Q˙ROS˙T˙UO¬P˙S˙Q˙T˙P˙Q¬P˙S˙Q˙T˙Q˙R¬P˙S˙Q˙T˙R˙P¬P˙S˙Q˙T˙S˙T¬P˙S˙Q˙T˙T˙U¬P˙S˙Q˙T˙U˙SP˙S˙Q˙T˙R˙US˙T˙UO
24 simp31 KHLPAQARASATAUAP˙Q˙ROS˙T˙UO¬P˙S˙Q˙T˙P˙Q¬P˙S˙Q˙T˙Q˙R¬P˙S˙Q˙T˙R˙P¬P˙S˙Q˙T˙S˙T¬P˙S˙Q˙T˙T˙U¬P˙S˙Q˙T˙U˙SP˙S˙Q˙T˙R˙U¬P˙S˙Q˙T˙P˙Q¬P˙S˙Q˙T˙Q˙R¬P˙S˙Q˙T˙R˙P
25 simp32 KHLPAQARASATAUAP˙Q˙ROS˙T˙UO¬P˙S˙Q˙T˙P˙Q¬P˙S˙Q˙T˙Q˙R¬P˙S˙Q˙T˙R˙P¬P˙S˙Q˙T˙S˙T¬P˙S˙Q˙T˙T˙U¬P˙S˙Q˙T˙U˙SP˙S˙Q˙T˙R˙U¬P˙S˙Q˙T˙S˙T¬P˙S˙Q˙T˙T˙U¬P˙S˙Q˙T˙U˙S
26 10 1 3 latmle1 KLatP˙SBaseKQ˙TBaseKP˙S˙Q˙T˙P˙S
27 7 12 16 26 syl3anc KHLPAQARASATAUAP˙Q˙ROS˙T˙UO¬P˙S˙Q˙T˙P˙Q¬P˙S˙Q˙T˙Q˙R¬P˙S˙Q˙T˙R˙P¬P˙S˙Q˙T˙S˙T¬P˙S˙Q˙T˙T˙U¬P˙S˙Q˙T˙U˙SP˙S˙Q˙T˙R˙UP˙S˙Q˙T˙P˙S
28 10 1 3 latmle2 KLatP˙SBaseKQ˙TBaseKP˙S˙Q˙T˙Q˙T
29 7 12 16 28 syl3anc KHLPAQARASATAUAP˙Q˙ROS˙T˙UO¬P˙S˙Q˙T˙P˙Q¬P˙S˙Q˙T˙Q˙R¬P˙S˙Q˙T˙R˙P¬P˙S˙Q˙T˙S˙T¬P˙S˙Q˙T˙T˙U¬P˙S˙Q˙T˙U˙SP˙S˙Q˙T˙R˙UP˙S˙Q˙T˙Q˙T
30 simp33 KHLPAQARASATAUAP˙Q˙ROS˙T˙UO¬P˙S˙Q˙T˙P˙Q¬P˙S˙Q˙T˙Q˙R¬P˙S˙Q˙T˙R˙P¬P˙S˙Q˙T˙S˙T¬P˙S˙Q˙T˙T˙U¬P˙S˙Q˙T˙U˙SP˙S˙Q˙T˙R˙UP˙S˙Q˙T˙R˙U
31 27 29 30 3jca KHLPAQARASATAUAP˙Q˙ROS˙T˙UO¬P˙S˙Q˙T˙P˙Q¬P˙S˙Q˙T˙Q˙R¬P˙S˙Q˙T˙R˙P¬P˙S˙Q˙T˙S˙T¬P˙S˙Q˙T˙T˙U¬P˙S˙Q˙T˙U˙SP˙S˙Q˙T˙R˙UP˙S˙Q˙T˙P˙SP˙S˙Q˙T˙Q˙TP˙S˙Q˙T˙R˙U
32 eqid P˙Q˙S˙T=P˙Q˙S˙T
33 eqid Q˙R˙T˙U=Q˙R˙T˙U
34 eqid R˙P˙U˙S=R˙P˙U˙S
35 10 1 2 4 3 5 32 33 34 dath2 KHLP˙S˙Q˙TBaseKPAQARASATAUAP˙Q˙ROS˙T˙UO¬P˙S˙Q˙T˙P˙Q¬P˙S˙Q˙T˙Q˙R¬P˙S˙Q˙T˙R˙P¬P˙S˙Q˙T˙S˙T¬P˙S˙Q˙T˙T˙U¬P˙S˙Q˙T˙U˙SP˙S˙Q˙T˙P˙SP˙S˙Q˙T˙Q˙TP˙S˙Q˙T˙R˙UP˙Q˙S˙T˙Q˙R˙T˙U˙R˙P˙U˙S
36 19 20 21 22 23 24 25 31 35 syl323anc KHLPAQARASATAUAP˙Q˙ROS˙T˙UO¬P˙S˙Q˙T˙P˙Q¬P˙S˙Q˙T˙Q˙R¬P˙S˙Q˙T˙R˙P¬P˙S˙Q˙T˙S˙T¬P˙S˙Q˙T˙T˙U¬P˙S˙Q˙T˙U˙SP˙S˙Q˙T˙R˙UP˙Q˙S˙T˙Q˙R˙T˙U˙R˙P˙U˙S