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 ) ) ) ) |