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 incom 
 |-  ( ( Y .+ ( X .+ Z ) ) i^i ( Y .+ W ) ) = ( ( Y .+ W ) i^i ( Y .+ ( X .+ Z ) ) )
4 simpl1 
 |-  ( ( ( K e. HL /\ X e. S /\ Y e. S ) /\ ( Z e. S /\ W e. S ) ) -> K e. HL )
5 simpl3 
 |-  ( ( ( K e. HL /\ X e. S /\ Y e. S ) /\ ( Z e. S /\ W e. S ) ) -> Y e. S )
6 eqid 
 |-  ( Atoms ` K ) = ( Atoms ` K )
7 6 1 psubssat 
 |-  ( ( K e. HL /\ Y e. S ) -> Y C_ ( Atoms ` K ) )
8 4 5 7 syl2anc 
 |-  ( ( ( K e. HL /\ X e. S /\ Y e. S ) /\ ( Z e. S /\ W e. S ) ) -> Y C_ ( Atoms ` K ) )
9 simpl2 
 |-  ( ( ( K e. HL /\ X e. S /\ Y e. S ) /\ ( Z e. S /\ W e. S ) ) -> X e. S )
10 6 1 psubssat 
 |-  ( ( K e. HL /\ X e. S ) -> X C_ ( Atoms ` K ) )
11 4 9 10 syl2anc 
 |-  ( ( ( K e. HL /\ X e. S /\ Y e. S ) /\ ( Z e. S /\ W e. S ) ) -> X C_ ( Atoms ` K ) )
12 simprl 
 |-  ( ( ( K e. HL /\ X e. S /\ Y e. S ) /\ ( Z e. S /\ W e. S ) ) -> Z e. S )
13 6 1 psubssat 
 |-  ( ( K e. HL /\ Z e. S ) -> Z C_ ( Atoms ` K ) )
14 4 12 13 syl2anc 
 |-  ( ( ( K e. HL /\ X e. S /\ Y e. S ) /\ ( Z e. S /\ W e. S ) ) -> Z C_ ( Atoms ` K ) )
15 6 2 paddssat 
 |-  ( ( K e. HL /\ X C_ ( Atoms ` K ) /\ Z C_ ( Atoms ` K ) ) -> ( X .+ Z ) C_ ( Atoms ` K ) )
16 4 11 14 15 syl3anc 
 |-  ( ( ( K e. HL /\ X e. S /\ Y e. S ) /\ ( Z e. S /\ W e. S ) ) -> ( X .+ Z ) C_ ( Atoms ` K ) )
17 simprr 
 |-  ( ( ( K e. HL /\ X e. S /\ Y e. S ) /\ ( Z e. S /\ W e. S ) ) -> W e. S )
18 1 2 paddclN 
 |-  ( ( K e. HL /\ Y e. S /\ W e. S ) -> ( Y .+ W ) e. S )
19 4 5 17 18 syl3anc 
 |-  ( ( ( K e. HL /\ X e. S /\ Y e. S ) /\ ( Z e. S /\ W e. S ) ) -> ( Y .+ W ) e. S )
20 6 1 psubssat 
 |-  ( ( K e. HL /\ W e. S ) -> W C_ ( Atoms ` K ) )
21 4 17 20 syl2anc 
 |-  ( ( ( K e. HL /\ X e. S /\ Y e. S ) /\ ( Z e. S /\ W e. S ) ) -> W C_ ( Atoms ` K ) )
22 6 2 sspadd1 
 |-  ( ( K e. HL /\ Y C_ ( Atoms ` K ) /\ W C_ ( Atoms ` K ) ) -> Y C_ ( Y .+ W ) )
23 4 8 21 22 syl3anc 
 |-  ( ( ( K e. HL /\ X e. S /\ Y e. S ) /\ ( Z e. S /\ W e. S ) ) -> Y C_ ( Y .+ W ) )
24 6 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 ) ) ) ) )
25 24 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 ) ) ) )
26 4 8 16 19 23 25 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 ) ) ) )
27 3 26 syl5reqr 
 |-  ( ( ( 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 16 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 6 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 4 11 8 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 6 2 paddass 
 |-  ( ( K e. HL /\ ( X C_ ( Atoms ` K ) /\ Y C_ ( Atoms ` K ) /\ Z C_ ( Atoms ` K ) ) ) -> ( ( X .+ Y ) .+ Z ) = ( X .+ ( Y .+ Z ) ) )
34 4 11 8 14 33 syl13anc 
 |-  ( ( ( K e. HL /\ X e. S /\ Y e. S ) /\ ( Z e. S /\ W e. S ) ) -> ( ( X .+ Y ) .+ Z ) = ( X .+ ( Y .+ Z ) ) )
35 6 2 padd12N 
 |-  ( ( K e. HL /\ ( X C_ ( Atoms ` K ) /\ Y C_ ( Atoms ` K ) /\ Z C_ ( Atoms ` K ) ) ) -> ( X .+ ( Y .+ Z ) ) = ( Y .+ ( X .+ Z ) ) )
36 4 11 8 14 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 6 2 paddass 
 |-  ( ( K e. HL /\ ( X C_ ( Atoms ` K ) /\ Y C_ ( Atoms ` K ) /\ W C_ ( Atoms ` K ) ) ) -> ( ( X .+ Y ) .+ W ) = ( X .+ ( Y .+ W ) ) )
39 4 11 8 21 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 6 1 psubssat 
 |-  ( ( K e. HL /\ ( Y .+ W ) e. S ) -> ( Y .+ W ) C_ ( Atoms ` K ) )
44 4 19 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 4 9 12 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 4 5 46 47 syl3anc 
 |-  ( ( ( K e. HL /\ X e. S /\ Y e. S ) /\ ( Z e. S /\ W e. S ) ) -> ( Y .+ ( X .+ Z ) ) e. S )
49 6 2 sspadd1 
 |-  ( ( K e. HL /\ X C_ ( Atoms ` K ) /\ Z C_ ( Atoms ` K ) ) -> X C_ ( X .+ Z ) )
50 4 11 14 49 syl3anc 
 |-  ( ( ( K e. HL /\ X e. S /\ Y e. S ) /\ ( Z e. S /\ W e. S ) ) -> X C_ ( X .+ Z ) )
51 6 2 sspadd2 
 |-  ( ( K e. HL /\ ( X .+ Z ) C_ ( Atoms ` K ) /\ Y C_ ( Atoms ` K ) ) -> ( X .+ Z ) C_ ( Y .+ ( X .+ Z ) ) )
52 4 16 8 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 6 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 4 11 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 ) ) ) )