Metamath Proof Explorer

Theorem 4atlem10b

Description: Lemma for 4at . Substitute V for R (cont.). (Contributed by NM, 10-Jul-2012)

Ref Expression
Hypotheses 4at.l 
|- .<_ = ( le ` K )
4at.j 
|- .\/ = ( join ` K )
4at.a 
|- A = ( Atoms ` K )
Assertion 4atlem10b 
|- ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A /\ V e. A ) /\ ( W e. A /\ -. R .<_ ( ( P .\/ Q ) .\/ W ) /\ -. S .<_ ( ( P .\/ Q ) .\/ R ) ) ) /\ ( R .<_ ( ( P .\/ Q ) .\/ ( V .\/ W ) ) /\ S .<_ ( ( P .\/ Q ) .\/ ( V .\/ W ) ) ) ) -> ( ( P .\/ Q ) .\/ ( R .\/ S ) ) = ( ( P .\/ Q ) .\/ ( V .\/ W ) ) )

Proof

Step Hyp Ref Expression
1 4at.l 
 |-  .<_ = ( le ` K )
2 4at.j 
 |-  .\/ = ( join ` K )
3 4at.a 
 |-  A = ( Atoms ` K )
4 simprr 
 |-  ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A /\ V e. A ) /\ ( W e. A /\ -. R .<_ ( ( P .\/ Q ) .\/ W ) /\ -. S .<_ ( ( P .\/ Q ) .\/ R ) ) ) /\ ( R .<_ ( ( P .\/ Q ) .\/ ( V .\/ W ) ) /\ S .<_ ( ( P .\/ Q ) .\/ ( V .\/ W ) ) ) ) -> S .<_ ( ( P .\/ Q ) .\/ ( V .\/ W ) ) )
5 simprl 
 |-  ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A /\ V e. A ) /\ ( W e. A /\ -. R .<_ ( ( P .\/ Q ) .\/ W ) /\ -. S .<_ ( ( P .\/ Q ) .\/ R ) ) ) /\ ( R .<_ ( ( P .\/ Q ) .\/ ( V .\/ W ) ) /\ S .<_ ( ( P .\/ Q ) .\/ ( V .\/ W ) ) ) ) -> R .<_ ( ( P .\/ Q ) .\/ ( V .\/ W ) ) )
6 simpl1 
 |-  ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A /\ V e. A ) /\ ( W e. A /\ -. R .<_ ( ( P .\/ Q ) .\/ W ) /\ -. S .<_ ( ( P .\/ Q ) .\/ R ) ) ) /\ ( R .<_ ( ( P .\/ Q ) .\/ ( V .\/ W ) ) /\ S .<_ ( ( P .\/ Q ) .\/ ( V .\/ W ) ) ) ) -> ( K e. HL /\ P e. A /\ Q e. A ) )
7 simpl21 
 |-  ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A /\ V e. A ) /\ ( W e. A /\ -. R .<_ ( ( P .\/ Q ) .\/ W ) /\ -. S .<_ ( ( P .\/ Q ) .\/ R ) ) ) /\ ( R .<_ ( ( P .\/ Q ) .\/ ( V .\/ W ) ) /\ S .<_ ( ( P .\/ Q ) .\/ ( V .\/ W ) ) ) ) -> R e. A )
8 simpl23 
 |-  ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A /\ V e. A ) /\ ( W e. A /\ -. R .<_ ( ( P .\/ Q ) .\/ W ) /\ -. S .<_ ( ( P .\/ Q ) .\/ R ) ) ) /\ ( R .<_ ( ( P .\/ Q ) .\/ ( V .\/ W ) ) /\ S .<_ ( ( P .\/ Q ) .\/ ( V .\/ W ) ) ) ) -> V e. A )
9 simpl31 
 |-  ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A /\ V e. A ) /\ ( W e. A /\ -. R .<_ ( ( P .\/ Q ) .\/ W ) /\ -. S .<_ ( ( P .\/ Q ) .\/ R ) ) ) /\ ( R .<_ ( ( P .\/ Q ) .\/ ( V .\/ W ) ) /\ S .<_ ( ( P .\/ Q ) .\/ ( V .\/ W ) ) ) ) -> W e. A )
10 simpl32 
 |-  ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A /\ V e. A ) /\ ( W e. A /\ -. R .<_ ( ( P .\/ Q ) .\/ W ) /\ -. S .<_ ( ( P .\/ Q ) .\/ R ) ) ) /\ ( R .<_ ( ( P .\/ Q ) .\/ ( V .\/ W ) ) /\ S .<_ ( ( P .\/ Q ) .\/ ( V .\/ W ) ) ) ) -> -. R .<_ ( ( P .\/ Q ) .\/ W ) )
11 1 2 3 4atlem10a 
 |-  ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ V e. A /\ W e. A ) /\ -. R .<_ ( ( P .\/ Q ) .\/ W ) ) -> ( R .<_ ( ( P .\/ Q ) .\/ ( V .\/ W ) ) <-> ( ( P .\/ Q ) .\/ ( R .\/ W ) ) = ( ( P .\/ Q ) .\/ ( V .\/ W ) ) ) )
12 6 7 8 9 10 11 syl131anc 
 |-  ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A /\ V e. A ) /\ ( W e. A /\ -. R .<_ ( ( P .\/ Q ) .\/ W ) /\ -. S .<_ ( ( P .\/ Q ) .\/ R ) ) ) /\ ( R .<_ ( ( P .\/ Q ) .\/ ( V .\/ W ) ) /\ S .<_ ( ( P .\/ Q ) .\/ ( V .\/ W ) ) ) ) -> ( R .<_ ( ( P .\/ Q ) .\/ ( V .\/ W ) ) <-> ( ( P .\/ Q ) .\/ ( R .\/ W ) ) = ( ( P .\/ Q ) .\/ ( V .\/ W ) ) ) )
13 5 12 mpbid 
 |-  ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A /\ V e. A ) /\ ( W e. A /\ -. R .<_ ( ( P .\/ Q ) .\/ W ) /\ -. S .<_ ( ( P .\/ Q ) .\/ R ) ) ) /\ ( R .<_ ( ( P .\/ Q ) .\/ ( V .\/ W ) ) /\ S .<_ ( ( P .\/ Q ) .\/ ( V .\/ W ) ) ) ) -> ( ( P .\/ Q ) .\/ ( R .\/ W ) ) = ( ( P .\/ Q ) .\/ ( V .\/ W ) ) )
14 4 13 breqtrrd 
 |-  ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A /\ V e. A ) /\ ( W e. A /\ -. R .<_ ( ( P .\/ Q ) .\/ W ) /\ -. S .<_ ( ( P .\/ Q ) .\/ R ) ) ) /\ ( R .<_ ( ( P .\/ Q ) .\/ ( V .\/ W ) ) /\ S .<_ ( ( P .\/ Q ) .\/ ( V .\/ W ) ) ) ) -> S .<_ ( ( P .\/ Q ) .\/ ( R .\/ W ) ) )
15 simpl22 
 |-  ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A /\ V e. A ) /\ ( W e. A /\ -. R .<_ ( ( P .\/ Q ) .\/ W ) /\ -. S .<_ ( ( P .\/ Q ) .\/ R ) ) ) /\ ( R .<_ ( ( P .\/ Q ) .\/ ( V .\/ W ) ) /\ S .<_ ( ( P .\/ Q ) .\/ ( V .\/ W ) ) ) ) -> S e. A )
16 simpl33 
 |-  ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A /\ V e. A ) /\ ( W e. A /\ -. R .<_ ( ( P .\/ Q ) .\/ W ) /\ -. S .<_ ( ( P .\/ Q ) .\/ R ) ) ) /\ ( R .<_ ( ( P .\/ Q ) .\/ ( V .\/ W ) ) /\ S .<_ ( ( P .\/ Q ) .\/ ( V .\/ W ) ) ) ) -> -. S .<_ ( ( P .\/ Q ) .\/ R ) )
17 1 2 3 4atlem9 
 |-  ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A /\ W e. A ) /\ -. S .<_ ( ( P .\/ Q ) .\/ R ) ) -> ( S .<_ ( ( P .\/ Q ) .\/ ( R .\/ W ) ) <-> ( ( P .\/ Q ) .\/ ( R .\/ S ) ) = ( ( P .\/ Q ) .\/ ( R .\/ W ) ) ) )
18 6 7 15 9 16 17 syl131anc 
 |-  ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A /\ V e. A ) /\ ( W e. A /\ -. R .<_ ( ( P .\/ Q ) .\/ W ) /\ -. S .<_ ( ( P .\/ Q ) .\/ R ) ) ) /\ ( R .<_ ( ( P .\/ Q ) .\/ ( V .\/ W ) ) /\ S .<_ ( ( P .\/ Q ) .\/ ( V .\/ W ) ) ) ) -> ( S .<_ ( ( P .\/ Q ) .\/ ( R .\/ W ) ) <-> ( ( P .\/ Q ) .\/ ( R .\/ S ) ) = ( ( P .\/ Q ) .\/ ( R .\/ W ) ) ) )
19 14 18 mpbid 
 |-  ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A /\ V e. A ) /\ ( W e. A /\ -. R .<_ ( ( P .\/ Q ) .\/ W ) /\ -. S .<_ ( ( P .\/ Q ) .\/ R ) ) ) /\ ( R .<_ ( ( P .\/ Q ) .\/ ( V .\/ W ) ) /\ S .<_ ( ( P .\/ Q ) .\/ ( V .\/ W ) ) ) ) -> ( ( P .\/ Q ) .\/ ( R .\/ S ) ) = ( ( P .\/ Q ) .\/ ( R .\/ W ) ) )
20 19 13 eqtrd 
 |-  ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A /\ V e. A ) /\ ( W e. A /\ -. R .<_ ( ( P .\/ Q ) .\/ W ) /\ -. S .<_ ( ( P .\/ Q ) .\/ R ) ) ) /\ ( R .<_ ( ( P .\/ Q ) .\/ ( V .\/ W ) ) /\ S .<_ ( ( P .\/ Q ) .\/ ( V .\/ W ) ) ) ) -> ( ( P .\/ Q ) .\/ ( R .\/ S ) ) = ( ( P .\/ Q ) .\/ ( V .\/ W ) ) )