Metamath Proof Explorer

Theorem pmodl42N

Description: Lemma derived from modular law. (Contributed by NM, 8-Apr-2012) (New usage is discouraged.)

Ref Expression
Hypotheses pmodl42.s 
|- S = ( PSubSp ` K )
pmodl42.p 
|- .+ = ( +P ` K )
Assertion pmodl42N 
|- ( ( ( K e. HL /\ X e. S /\ Y e. S ) /\ ( Z e. S /\ W e. S ) ) -> ( ( ( X .+ Y ) .+ Z ) i^i ( ( X .+ Y ) .+ W ) ) = ( ( X .+ Y ) .+ ( ( X .+ Z ) i^i ( Y .+ W ) ) ) )

Proof

Step Hyp Ref Expression
1 pmodl42.s 
 |-  S = ( PSubSp ` K )
2 pmodl42.p 
 |-  .+ = ( +P ` K )
3 simpl1 
 |-  ( ( ( K e. HL /\ X e. S /\ Y e. S ) /\ ( Z e. S /\ W e. S ) ) -> K e. HL )
4 simpl3 
 |-  ( ( ( K e. HL /\ X e. S /\ Y e. S ) /\ ( Z e. S /\ W e. S ) ) -> Y e. S )
5 eqid 
 |-  ( Atoms ` K ) = ( Atoms ` K )
6 5 1 psubssat 
 |-  ( ( K e. HL /\ Y e. S ) -> Y C_ ( Atoms ` K ) )
7 3 4 6 syl2anc 
 |-  ( ( ( K e. HL /\ X e. S /\ Y e. S ) /\ ( Z e. S /\ W e. S ) ) -> Y C_ ( Atoms ` K ) )
8 simpl2 
 |-  ( ( ( K e. HL /\ X e. S /\ Y e. S ) /\ ( Z e. S /\ W e. S ) ) -> X e. S )
9 5 1 psubssat 
 |-  ( ( K e. HL /\ X e. S ) -> X C_ ( Atoms ` K ) )
10 3 8 9 syl2anc 
 |-  ( ( ( K e. HL /\ X e. S /\ Y e. S ) /\ ( Z e. S /\ W e. S ) ) -> X C_ ( Atoms ` K ) )
11 simprl 
 |-  ( ( ( K e. HL /\ X e. S /\ Y e. S ) /\ ( Z e. S /\ W e. S ) ) -> Z e. S )
12 5 1 psubssat 
 |-  ( ( K e. HL /\ Z e. S ) -> Z C_ ( Atoms ` K ) )
13 3 11 12 syl2anc 
 |-  ( ( ( K e. HL /\ X e. S /\ Y e. S ) /\ ( Z e. S /\ W e. S ) ) -> Z C_ ( Atoms ` K ) )
14 5 2 paddssat 
 |-  ( ( K e. HL /\ X C_ ( Atoms ` K ) /\ Z C_ ( Atoms ` K ) ) -> ( X .+ Z ) C_ ( Atoms ` K ) )
15 3 10 13 14 syl3anc 
 |-  ( ( ( K e. HL /\ X e. S /\ Y e. S ) /\ ( Z e. S /\ W e. S ) ) -> ( X .+ Z ) C_ ( Atoms ` K ) )
16 simprr 
 |-  ( ( ( K e. HL /\ X e. S /\ Y e. S ) /\ ( Z e. S /\ W e. S ) ) -> W e. S )
17 1 2 paddclN 
 |-  ( ( K e. HL /\ Y e. S /\ W e. S ) -> ( Y .+ W ) e. S )
18 3 4 16 17 syl3anc 
 |-  ( ( ( K e. HL /\ X e. S /\ Y e. S ) /\ ( Z e. S /\ W e. S ) ) -> ( Y .+ W ) e. S )
19 5 1 psubssat 
 |-  ( ( K e. HL /\ W e. S ) -> W C_ ( Atoms ` K ) )
20 3 16 19 syl2anc 
 |-  ( ( ( K e. HL /\ X e. S /\ Y e. S ) /\ ( Z e. S /\ W e. S ) ) -> W C_ ( Atoms ` K ) )
21 5 2 sspadd1 
 |-  ( ( K e. HL /\ Y C_ ( Atoms ` K ) /\ W C_ ( Atoms ` K ) ) -> Y C_ ( Y .+ W ) )
22 3 7 20 21 syl3anc 
 |-  ( ( ( K e. HL /\ X e. S /\ Y e. S ) /\ ( Z e. S /\ W e. S ) ) -> Y C_ ( Y .+ W ) )
23 5 1 2 pmod1i 
 |-  ( ( K e. HL /\ ( Y C_ ( Atoms ` K ) /\ ( X .+ Z ) C_ ( Atoms ` K ) /\ ( Y .+ W ) e. S ) ) -> ( Y C_ ( Y .+ W ) -> ( ( Y .+ ( X .+ Z ) ) i^i ( Y .+ W ) ) = ( Y .+ ( ( X .+ Z ) i^i ( Y .+ W ) ) ) ) )
24 23 3impia 
 |-  ( ( K e. HL /\ ( Y C_ ( Atoms ` K ) /\ ( X .+ Z ) C_ ( Atoms ` K ) /\ ( Y .+ W ) e. S ) /\ Y C_ ( Y .+ W ) ) -> ( ( Y .+ ( X .+ Z ) ) i^i ( Y .+ W ) ) = ( Y .+ ( ( X .+ Z ) i^i ( Y .+ W ) ) ) )
25 3 7 15 18 22 24 syl131anc 
 |-  ( ( ( K e. HL /\ X e. S /\ Y e. S ) /\ ( Z e. S /\ W e. S ) ) -> ( ( Y .+ ( X .+ Z ) ) i^i ( Y .+ W ) ) = ( Y .+ ( ( X .+ Z ) i^i ( Y .+ W ) ) ) )
26 incom 
 |-  ( ( Y .+ ( X .+ Z ) ) i^i ( Y .+ W ) ) = ( ( Y .+ W ) i^i ( Y .+ ( X .+ Z ) ) )
27 25 26 eqtr3di 
 |-  ( ( ( K e. HL /\ X e. S /\ Y e. S ) /\ ( Z e. S /\ W e. S ) ) -> ( Y .+ ( ( X .+ Z ) i^i ( Y .+ W ) ) ) = ( ( Y .+ W ) i^i ( Y .+ ( X .+ Z ) ) ) )
28 27 oveq2d 
 |-  ( ( ( K e. HL /\ X e. S /\ Y e. S ) /\ ( Z e. S /\ W e. S ) ) -> ( X .+ ( Y .+ ( ( X .+ Z ) i^i ( Y .+ W ) ) ) ) = ( X .+ ( ( Y .+ W ) i^i ( Y .+ ( X .+ Z ) ) ) ) )
29 ssinss1 
 |-  ( ( X .+ Z ) C_ ( Atoms ` K ) -> ( ( X .+ Z ) i^i ( Y .+ W ) ) C_ ( Atoms ` K ) )
30 15 29 syl 
 |-  ( ( ( K e. HL /\ X e. S /\ Y e. S ) /\ ( Z e. S /\ W e. S ) ) -> ( ( X .+ Z ) i^i ( Y .+ W ) ) C_ ( Atoms ` K ) )
31 5 2 paddass 
 |-  ( ( K e. HL /\ ( X C_ ( Atoms ` K ) /\ Y C_ ( Atoms ` K ) /\ ( ( X .+ Z ) i^i ( Y .+ W ) ) C_ ( Atoms ` K ) ) ) -> ( ( X .+ Y ) .+ ( ( X .+ Z ) i^i ( Y .+ W ) ) ) = ( X .+ ( Y .+ ( ( X .+ Z ) i^i ( Y .+ W ) ) ) ) )
32 3 10 7 30 31 syl13anc 
 |-  ( ( ( K e. HL /\ X e. S /\ Y e. S ) /\ ( Z e. S /\ W e. S ) ) -> ( ( X .+ Y ) .+ ( ( X .+ Z ) i^i ( Y .+ W ) ) ) = ( X .+ ( Y .+ ( ( X .+ Z ) i^i ( Y .+ W ) ) ) ) )
33 5 2 paddass 
 |-  ( ( K e. HL /\ ( X C_ ( Atoms ` K ) /\ Y C_ ( Atoms ` K ) /\ Z C_ ( Atoms ` K ) ) ) -> ( ( X .+ Y ) .+ Z ) = ( X .+ ( Y .+ Z ) ) )
34 3 10 7 13 33 syl13anc 
 |-  ( ( ( K e. HL /\ X e. S /\ Y e. S ) /\ ( Z e. S /\ W e. S ) ) -> ( ( X .+ Y ) .+ Z ) = ( X .+ ( Y .+ Z ) ) )
35 5 2 padd12N 
 |-  ( ( K e. HL /\ ( X C_ ( Atoms ` K ) /\ Y C_ ( Atoms ` K ) /\ Z C_ ( Atoms ` K ) ) ) -> ( X .+ ( Y .+ Z ) ) = ( Y .+ ( X .+ Z ) ) )
36 3 10 7 13 35 syl13anc 
 |-  ( ( ( K e. HL /\ X e. S /\ Y e. S ) /\ ( Z e. S /\ W e. S ) ) -> ( X .+ ( Y .+ Z ) ) = ( Y .+ ( X .+ Z ) ) )
37 34 36 eqtrd 
 |-  ( ( ( K e. HL /\ X e. S /\ Y e. S ) /\ ( Z e. S /\ W e. S ) ) -> ( ( X .+ Y ) .+ Z ) = ( Y .+ ( X .+ Z ) ) )
38 5 2 paddass 
 |-  ( ( K e. HL /\ ( X C_ ( Atoms ` K ) /\ Y C_ ( Atoms ` K ) /\ W C_ ( Atoms ` K ) ) ) -> ( ( X .+ Y ) .+ W ) = ( X .+ ( Y .+ W ) ) )
39 3 10 7 20 38 syl13anc 
 |-  ( ( ( K e. HL /\ X e. S /\ Y e. S ) /\ ( Z e. S /\ W e. S ) ) -> ( ( X .+ Y ) .+ W ) = ( X .+ ( Y .+ W ) ) )
40 37 39 ineq12d 
 |-  ( ( ( K e. HL /\ X e. S /\ Y e. S ) /\ ( Z e. S /\ W e. S ) ) -> ( ( ( X .+ Y ) .+ Z ) i^i ( ( X .+ Y ) .+ W ) ) = ( ( Y .+ ( X .+ Z ) ) i^i ( X .+ ( Y .+ W ) ) ) )
41 incom 
 |-  ( ( Y .+ ( X .+ Z ) ) i^i ( X .+ ( Y .+ W ) ) ) = ( ( X .+ ( Y .+ W ) ) i^i ( Y .+ ( X .+ Z ) ) )
42 40 41 eqtrdi 
 |-  ( ( ( K e. HL /\ X e. S /\ Y e. S ) /\ ( Z e. S /\ W e. S ) ) -> ( ( ( X .+ Y ) .+ Z ) i^i ( ( X .+ Y ) .+ W ) ) = ( ( X .+ ( Y .+ W ) ) i^i ( Y .+ ( X .+ Z ) ) ) )
43 5 1 psubssat 
 |-  ( ( K e. HL /\ ( Y .+ W ) e. S ) -> ( Y .+ W ) C_ ( Atoms ` K ) )
44 3 18 43 syl2anc 
 |-  ( ( ( K e. HL /\ X e. S /\ Y e. S ) /\ ( Z e. S /\ W e. S ) ) -> ( Y .+ W ) C_ ( Atoms ` K ) )
45 1 2 paddclN 
 |-  ( ( K e. HL /\ X e. S /\ Z e. S ) -> ( X .+ Z ) e. S )
46 3 8 11 45 syl3anc 
 |-  ( ( ( K e. HL /\ X e. S /\ Y e. S ) /\ ( Z e. S /\ W e. S ) ) -> ( X .+ Z ) e. S )
47 1 2 paddclN 
 |-  ( ( K e. HL /\ Y e. S /\ ( X .+ Z ) e. S ) -> ( Y .+ ( X .+ Z ) ) e. S )
48 3 4 46 47 syl3anc 
 |-  ( ( ( K e. HL /\ X e. S /\ Y e. S ) /\ ( Z e. S /\ W e. S ) ) -> ( Y .+ ( X .+ Z ) ) e. S )
49 5 2 sspadd1 
 |-  ( ( K e. HL /\ X C_ ( Atoms ` K ) /\ Z C_ ( Atoms ` K ) ) -> X C_ ( X .+ Z ) )
50 3 10 13 49 syl3anc 
 |-  ( ( ( K e. HL /\ X e. S /\ Y e. S ) /\ ( Z e. S /\ W e. S ) ) -> X C_ ( X .+ Z ) )
51 5 2 sspadd2 
 |-  ( ( K e. HL /\ ( X .+ Z ) C_ ( Atoms ` K ) /\ Y C_ ( Atoms ` K ) ) -> ( X .+ Z ) C_ ( Y .+ ( X .+ Z ) ) )
52 3 15 7 51 syl3anc 
 |-  ( ( ( K e. HL /\ X e. S /\ Y e. S ) /\ ( Z e. S /\ W e. S ) ) -> ( X .+ Z ) C_ ( Y .+ ( X .+ Z ) ) )
53 50 52 sstrd 
 |-  ( ( ( K e. HL /\ X e. S /\ Y e. S ) /\ ( Z e. S /\ W e. S ) ) -> X C_ ( Y .+ ( X .+ Z ) ) )
54 5 1 2 pmod1i 
 |-  ( ( K e. HL /\ ( X C_ ( Atoms ` K ) /\ ( Y .+ W ) C_ ( Atoms ` K ) /\ ( Y .+ ( X .+ Z ) ) e. S ) ) -> ( X C_ ( Y .+ ( X .+ Z ) ) -> ( ( X .+ ( Y .+ W ) ) i^i ( Y .+ ( X .+ Z ) ) ) = ( X .+ ( ( Y .+ W ) i^i ( Y .+ ( X .+ Z ) ) ) ) ) )
55 54 3impia 
 |-  ( ( K e. HL /\ ( X C_ ( Atoms ` K ) /\ ( Y .+ W ) C_ ( Atoms ` K ) /\ ( Y .+ ( X .+ Z ) ) e. S ) /\ X C_ ( Y .+ ( X .+ Z ) ) ) -> ( ( X .+ ( Y .+ W ) ) i^i ( Y .+ ( X .+ Z ) ) ) = ( X .+ ( ( Y .+ W ) i^i ( Y .+ ( X .+ Z ) ) ) ) )
56 3 10 44 48 53 55 syl131anc 
 |-  ( ( ( K e. HL /\ X e. S /\ Y e. S ) /\ ( Z e. S /\ W e. S ) ) -> ( ( X .+ ( Y .+ W ) ) i^i ( Y .+ ( X .+ Z ) ) ) = ( X .+ ( ( Y .+ W ) i^i ( Y .+ ( X .+ Z ) ) ) ) )
57 42 56 eqtrd 
 |-  ( ( ( K e. HL /\ X e. S /\ Y e. S ) /\ ( Z e. S /\ W e. S ) ) -> ( ( ( X .+ Y ) .+ Z ) i^i ( ( X .+ Y ) .+ W ) ) = ( X .+ ( ( Y .+ W ) i^i ( Y .+ ( X .+ Z ) ) ) ) )
58 28 32 57 3eqtr4rd 
 |-  ( ( ( K e. HL /\ X e. S /\ Y e. S ) /\ ( Z e. S /\ W e. S ) ) -> ( ( ( X .+ Y ) .+ Z ) i^i ( ( X .+ Y ) .+ W ) ) = ( ( X .+ Y ) .+ ( ( X .+ Z ) i^i ( Y .+ W ) ) ) )