Metamath Proof Explorer

Theorem pmodlem2

Description: Lemma for pmod1i . (Contributed by NM, 9-Mar-2012)

Ref Expression
Hypotheses pmodlem.l 
|- .<_ = ( le ` K )
pmodlem.j 
|- .\/ = ( join ` K )
pmodlem.a 
|- A = ( Atoms ` K )
pmodlem.s 
|- S = ( PSubSp ` K )
pmodlem.p 
|- .+ = ( +P ` K )
Assertion pmodlem2 
|- ( ( K e. HL /\ ( X C_ A /\ Y C_ A /\ Z e. S ) /\ X C_ Z ) -> ( ( X .+ Y ) i^i Z ) C_ ( X .+ ( Y i^i Z ) ) )

Proof

Step Hyp Ref Expression
1 pmodlem.l 
 |-  .<_ = ( le ` K )
2 pmodlem.j 
 |-  .\/ = ( join ` K )
3 pmodlem.a 
 |-  A = ( Atoms ` K )
4 pmodlem.s 
 |-  S = ( PSubSp ` K )
5 pmodlem.p 
 |-  .+ = ( +P ` K )
6 simpr 
 |-  ( ( ( K e. HL /\ ( X C_ A /\ Y C_ A /\ Z e. S ) /\ X C_ Z ) /\ X = (/) ) -> X = (/) )
7 6 oveq1d 
 |-  ( ( ( K e. HL /\ ( X C_ A /\ Y C_ A /\ Z e. S ) /\ X C_ Z ) /\ X = (/) ) -> ( X .+ Y ) = ( (/) .+ Y ) )
8 simpl1 
 |-  ( ( ( K e. HL /\ ( X C_ A /\ Y C_ A /\ Z e. S ) /\ X C_ Z ) /\ X = (/) ) -> K e. HL )
9 simpl22 
 |-  ( ( ( K e. HL /\ ( X C_ A /\ Y C_ A /\ Z e. S ) /\ X C_ Z ) /\ X = (/) ) -> Y C_ A )
10 3 5 padd02 
 |-  ( ( K e. HL /\ Y C_ A ) -> ( (/) .+ Y ) = Y )
11 8 9 10 syl2anc 
 |-  ( ( ( K e. HL /\ ( X C_ A /\ Y C_ A /\ Z e. S ) /\ X C_ Z ) /\ X = (/) ) -> ( (/) .+ Y ) = Y )
12 7 11 eqtrd 
 |-  ( ( ( K e. HL /\ ( X C_ A /\ Y C_ A /\ Z e. S ) /\ X C_ Z ) /\ X = (/) ) -> ( X .+ Y ) = Y )
13 12 ineq1d 
 |-  ( ( ( K e. HL /\ ( X C_ A /\ Y C_ A /\ Z e. S ) /\ X C_ Z ) /\ X = (/) ) -> ( ( X .+ Y ) i^i Z ) = ( Y i^i Z ) )
14 ssinss1 
 |-  ( Y C_ A -> ( Y i^i Z ) C_ A )
15 9 14 syl 
 |-  ( ( ( K e. HL /\ ( X C_ A /\ Y C_ A /\ Z e. S ) /\ X C_ Z ) /\ X = (/) ) -> ( Y i^i Z ) C_ A )
16 simpl21 
 |-  ( ( ( K e. HL /\ ( X C_ A /\ Y C_ A /\ Z e. S ) /\ X C_ Z ) /\ X = (/) ) -> X C_ A )
17 3 5 sspadd2 
 |-  ( ( K e. HL /\ ( Y i^i Z ) C_ A /\ X C_ A ) -> ( Y i^i Z ) C_ ( X .+ ( Y i^i Z ) ) )
18 8 15 16 17 syl3anc 
 |-  ( ( ( K e. HL /\ ( X C_ A /\ Y C_ A /\ Z e. S ) /\ X C_ Z ) /\ X = (/) ) -> ( Y i^i Z ) C_ ( X .+ ( Y i^i Z ) ) )
19 13 18 eqsstrd 
 |-  ( ( ( K e. HL /\ ( X C_ A /\ Y C_ A /\ Z e. S ) /\ X C_ Z ) /\ X = (/) ) -> ( ( X .+ Y ) i^i Z ) C_ ( X .+ ( Y i^i Z ) ) )
20 oveq2 
 |-  ( Y = (/) -> ( X .+ Y ) = ( X .+ (/) ) )
21 simp1 
 |-  ( ( K e. HL /\ ( X C_ A /\ Y C_ A /\ Z e. S ) /\ X C_ Z ) -> K e. HL )
22 simp21 
 |-  ( ( K e. HL /\ ( X C_ A /\ Y C_ A /\ Z e. S ) /\ X C_ Z ) -> X C_ A )
23 3 5 padd01 
 |-  ( ( K e. HL /\ X C_ A ) -> ( X .+ (/) ) = X )
24 21 22 23 syl2anc 
 |-  ( ( K e. HL /\ ( X C_ A /\ Y C_ A /\ Z e. S ) /\ X C_ Z ) -> ( X .+ (/) ) = X )
25 20 24 sylan9eqr 
 |-  ( ( ( K e. HL /\ ( X C_ A /\ Y C_ A /\ Z e. S ) /\ X C_ Z ) /\ Y = (/) ) -> ( X .+ Y ) = X )
26 25 ineq1d 
 |-  ( ( ( K e. HL /\ ( X C_ A /\ Y C_ A /\ Z e. S ) /\ X C_ Z ) /\ Y = (/) ) -> ( ( X .+ Y ) i^i Z ) = ( X i^i Z ) )
27 inss1 
 |-  ( X i^i Z ) C_ X
28 simpl1 
 |-  ( ( ( K e. HL /\ ( X C_ A /\ Y C_ A /\ Z e. S ) /\ X C_ Z ) /\ Y = (/) ) -> K e. HL )
29 simpl21 
 |-  ( ( ( K e. HL /\ ( X C_ A /\ Y C_ A /\ Z e. S ) /\ X C_ Z ) /\ Y = (/) ) -> X C_ A )
30 simpl22 
 |-  ( ( ( K e. HL /\ ( X C_ A /\ Y C_ A /\ Z e. S ) /\ X C_ Z ) /\ Y = (/) ) -> Y C_ A )
31 30 14 syl 
 |-  ( ( ( K e. HL /\ ( X C_ A /\ Y C_ A /\ Z e. S ) /\ X C_ Z ) /\ Y = (/) ) -> ( Y i^i Z ) C_ A )
32 3 5 sspadd1 
 |-  ( ( K e. HL /\ X C_ A /\ ( Y i^i Z ) C_ A ) -> X C_ ( X .+ ( Y i^i Z ) ) )
33 28 29 31 32 syl3anc 
 |-  ( ( ( K e. HL /\ ( X C_ A /\ Y C_ A /\ Z e. S ) /\ X C_ Z ) /\ Y = (/) ) -> X C_ ( X .+ ( Y i^i Z ) ) )
34 27 33 sstrid 
 |-  ( ( ( K e. HL /\ ( X C_ A /\ Y C_ A /\ Z e. S ) /\ X C_ Z ) /\ Y = (/) ) -> ( X i^i Z ) C_ ( X .+ ( Y i^i Z ) ) )
35 26 34 eqsstrd 
 |-  ( ( ( K e. HL /\ ( X C_ A /\ Y C_ A /\ Z e. S ) /\ X C_ Z ) /\ Y = (/) ) -> ( ( X .+ Y ) i^i Z ) C_ ( X .+ ( Y i^i Z ) ) )
36 elin 
 |-  ( p e. ( ( X .+ Y ) i^i Z ) <-> ( p e. ( X .+ Y ) /\ p e. Z ) )
37 simpl1 
 |-  ( ( ( K e. HL /\ ( X C_ A /\ Y C_ A /\ Z e. S ) /\ X C_ Z ) /\ ( ( X =/= (/) /\ Y =/= (/) ) /\ p e. Z ) ) -> K e. HL )
38 37 hllatd 
 |-  ( ( ( K e. HL /\ ( X C_ A /\ Y C_ A /\ Z e. S ) /\ X C_ Z ) /\ ( ( X =/= (/) /\ Y =/= (/) ) /\ p e. Z ) ) -> K e. Lat )
39 simpl21 
 |-  ( ( ( K e. HL /\ ( X C_ A /\ Y C_ A /\ Z e. S ) /\ X C_ Z ) /\ ( ( X =/= (/) /\ Y =/= (/) ) /\ p e. Z ) ) -> X C_ A )
40 simpl22 
 |-  ( ( ( K e. HL /\ ( X C_ A /\ Y C_ A /\ Z e. S ) /\ X C_ Z ) /\ ( ( X =/= (/) /\ Y =/= (/) ) /\ p e. Z ) ) -> Y C_ A )
41 simprl 
 |-  ( ( ( K e. HL /\ ( X C_ A /\ Y C_ A /\ Z e. S ) /\ X C_ Z ) /\ ( ( X =/= (/) /\ Y =/= (/) ) /\ p e. Z ) ) -> ( X =/= (/) /\ Y =/= (/) ) )
42 1 2 3 5 elpaddn0 
 |-  ( ( ( K e. Lat /\ X C_ A /\ Y C_ A ) /\ ( X =/= (/) /\ Y =/= (/) ) ) -> ( p e. ( X .+ Y ) <-> ( p e. A /\ E. q e. X E. r e. Y p .<_ ( q .\/ r ) ) ) )
43 38 39 40 41 42 syl31anc 
 |-  ( ( ( K e. HL /\ ( X C_ A /\ Y C_ A /\ Z e. S ) /\ X C_ Z ) /\ ( ( X =/= (/) /\ Y =/= (/) ) /\ p e. Z ) ) -> ( p e. ( X .+ Y ) <-> ( p e. A /\ E. q e. X E. r e. Y p .<_ ( q .\/ r ) ) ) )
44 simpl1 
 |-  ( ( ( K e. HL /\ ( X C_ A /\ Y C_ A /\ Z e. S ) /\ X C_ Z ) /\ ( p e. Z /\ ( q e. X /\ r e. Y ) /\ p .<_ ( q .\/ r ) ) ) -> K e. HL )
45 simpl21 
 |-  ( ( ( K e. HL /\ ( X C_ A /\ Y C_ A /\ Z e. S ) /\ X C_ Z ) /\ ( p e. Z /\ ( q e. X /\ r e. Y ) /\ p .<_ ( q .\/ r ) ) ) -> X C_ A )
46 simpl22 
 |-  ( ( ( K e. HL /\ ( X C_ A /\ Y C_ A /\ Z e. S ) /\ X C_ Z ) /\ ( p e. Z /\ ( q e. X /\ r e. Y ) /\ p .<_ ( q .\/ r ) ) ) -> Y C_ A )
47 simpl23 
 |-  ( ( ( K e. HL /\ ( X C_ A /\ Y C_ A /\ Z e. S ) /\ X C_ Z ) /\ ( p e. Z /\ ( q e. X /\ r e. Y ) /\ p .<_ ( q .\/ r ) ) ) -> Z e. S )
48 simpl3 
 |-  ( ( ( K e. HL /\ ( X C_ A /\ Y C_ A /\ Z e. S ) /\ X C_ Z ) /\ ( p e. Z /\ ( q e. X /\ r e. Y ) /\ p .<_ ( q .\/ r ) ) ) -> X C_ Z )
49 simpr1 
 |-  ( ( ( K e. HL /\ ( X C_ A /\ Y C_ A /\ Z e. S ) /\ X C_ Z ) /\ ( p e. Z /\ ( q e. X /\ r e. Y ) /\ p .<_ ( q .\/ r ) ) ) -> p e. Z )
50 simpr2l 
 |-  ( ( ( K e. HL /\ ( X C_ A /\ Y C_ A /\ Z e. S ) /\ X C_ Z ) /\ ( p e. Z /\ ( q e. X /\ r e. Y ) /\ p .<_ ( q .\/ r ) ) ) -> q e. X )
51 simpr2r 
 |-  ( ( ( K e. HL /\ ( X C_ A /\ Y C_ A /\ Z e. S ) /\ X C_ Z ) /\ ( p e. Z /\ ( q e. X /\ r e. Y ) /\ p .<_ ( q .\/ r ) ) ) -> r e. Y )
52 simpr3 
 |-  ( ( ( K e. HL /\ ( X C_ A /\ Y C_ A /\ Z e. S ) /\ X C_ Z ) /\ ( p e. Z /\ ( q e. X /\ r e. Y ) /\ p .<_ ( q .\/ r ) ) ) -> p .<_ ( q .\/ r ) )
53 1 2 3 4 5 pmodlem1 
 |-  ( ( ( K e. HL /\ X C_ A /\ Y C_ A ) /\ ( Z e. S /\ X C_ Z /\ p e. Z ) /\ ( q e. X /\ r e. Y /\ p .<_ ( q .\/ r ) ) ) -> p e. ( X .+ ( Y i^i Z ) ) )
54 44 45 46 47 48 49 50 51 52 53 syl333anc 
 |-  ( ( ( K e. HL /\ ( X C_ A /\ Y C_ A /\ Z e. S ) /\ X C_ Z ) /\ ( p e. Z /\ ( q e. X /\ r e. Y ) /\ p .<_ ( q .\/ r ) ) ) -> p e. ( X .+ ( Y i^i Z ) ) )
55 54 3exp2 
 |-  ( ( K e. HL /\ ( X C_ A /\ Y C_ A /\ Z e. S ) /\ X C_ Z ) -> ( p e. Z -> ( ( q e. X /\ r e. Y ) -> ( p .<_ ( q .\/ r ) -> p e. ( X .+ ( Y i^i Z ) ) ) ) ) )
56 55 imp 
 |-  ( ( ( K e. HL /\ ( X C_ A /\ Y C_ A /\ Z e. S ) /\ X C_ Z ) /\ p e. Z ) -> ( ( q e. X /\ r e. Y ) -> ( p .<_ ( q .\/ r ) -> p e. ( X .+ ( Y i^i Z ) ) ) ) )
57 56 rexlimdvv 
 |-  ( ( ( K e. HL /\ ( X C_ A /\ Y C_ A /\ Z e. S ) /\ X C_ Z ) /\ p e. Z ) -> ( E. q e. X E. r e. Y p .<_ ( q .\/ r ) -> p e. ( X .+ ( Y i^i Z ) ) ) )
58 57 adantld 
 |-  ( ( ( K e. HL /\ ( X C_ A /\ Y C_ A /\ Z e. S ) /\ X C_ Z ) /\ p e. Z ) -> ( ( p e. A /\ E. q e. X E. r e. Y p .<_ ( q .\/ r ) ) -> p e. ( X .+ ( Y i^i Z ) ) ) )
59 58 adantrl 
 |-  ( ( ( K e. HL /\ ( X C_ A /\ Y C_ A /\ Z e. S ) /\ X C_ Z ) /\ ( ( X =/= (/) /\ Y =/= (/) ) /\ p e. Z ) ) -> ( ( p e. A /\ E. q e. X E. r e. Y p .<_ ( q .\/ r ) ) -> p e. ( X .+ ( Y i^i Z ) ) ) )
60 43 59 sylbid 
 |-  ( ( ( K e. HL /\ ( X C_ A /\ Y C_ A /\ Z e. S ) /\ X C_ Z ) /\ ( ( X =/= (/) /\ Y =/= (/) ) /\ p e. Z ) ) -> ( p e. ( X .+ Y ) -> p e. ( X .+ ( Y i^i Z ) ) ) )
61 60 exp32 
 |-  ( ( K e. HL /\ ( X C_ A /\ Y C_ A /\ Z e. S ) /\ X C_ Z ) -> ( ( X =/= (/) /\ Y =/= (/) ) -> ( p e. Z -> ( p e. ( X .+ Y ) -> p e. ( X .+ ( Y i^i Z ) ) ) ) ) )
62 61 com34 
 |-  ( ( K e. HL /\ ( X C_ A /\ Y C_ A /\ Z e. S ) /\ X C_ Z ) -> ( ( X =/= (/) /\ Y =/= (/) ) -> ( p e. ( X .+ Y ) -> ( p e. Z -> p e. ( X .+ ( Y i^i Z ) ) ) ) ) )
63 62 imp4b 
 |-  ( ( ( K e. HL /\ ( X C_ A /\ Y C_ A /\ Z e. S ) /\ X C_ Z ) /\ ( X =/= (/) /\ Y =/= (/) ) ) -> ( ( p e. ( X .+ Y ) /\ p e. Z ) -> p e. ( X .+ ( Y i^i Z ) ) ) )
64 36 63 syl5bi 
 |-  ( ( ( K e. HL /\ ( X C_ A /\ Y C_ A /\ Z e. S ) /\ X C_ Z ) /\ ( X =/= (/) /\ Y =/= (/) ) ) -> ( p e. ( ( X .+ Y ) i^i Z ) -> p e. ( X .+ ( Y i^i Z ) ) ) )
65 64 ssrdv 
 |-  ( ( ( K e. HL /\ ( X C_ A /\ Y C_ A /\ Z e. S ) /\ X C_ Z ) /\ ( X =/= (/) /\ Y =/= (/) ) ) -> ( ( X .+ Y ) i^i Z ) C_ ( X .+ ( Y i^i Z ) ) )
66 19 35 65 pm2.61da2ne 
 |-  ( ( K e. HL /\ ( X C_ A /\ Y C_ A /\ Z e. S ) /\ X C_ Z ) -> ( ( X .+ Y ) i^i Z ) C_ ( X .+ ( Y i^i Z ) ) )