This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem pmod1i

Description: The modular law holds in a projective subspace. (Contributed by NM, 10-Mar-2012)

Ref Expression
Hypotheses pmod.a 
|- A = ( Atoms ` K )
pmod.s 
|- S = ( PSubSp ` K )
pmod.p 
|- .+ = ( +P ` K )
Assertion pmod1i 
|- ( ( K e. HL /\ ( X C_ A /\ Y C_ A /\ Z e. S ) ) -> ( X C_ Z -> ( ( X .+ Y ) i^i Z ) = ( X .+ ( Y i^i Z ) ) ) )

Proof

Step Hyp Ref Expression
1 pmod.a 
 |-  A = ( Atoms ` K )
2 pmod.s 
 |-  S = ( PSubSp ` K )
3 pmod.p 
 |-  .+ = ( +P ` K )
4 eqid 
 |-  ( le ` K ) = ( le ` K )
5 eqid 
 |-  ( join ` K ) = ( join ` K )
6 4 5 1 2 3 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 ) ) )
7 6 3expa 
 |-  ( ( ( 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 ) ) )
8 inss1 
 |-  ( Y i^i Z ) C_ Y
9 simpll 
 |-  ( ( ( K e. HL /\ ( X C_ A /\ Y C_ A /\ Z e. S ) ) /\ X C_ Z ) -> K e. HL )
10 simplr2 
 |-  ( ( ( K e. HL /\ ( X C_ A /\ Y C_ A /\ Z e. S ) ) /\ X C_ Z ) -> Y C_ A )
11 simplr1 
 |-  ( ( ( K e. HL /\ ( X C_ A /\ Y C_ A /\ Z e. S ) ) /\ X C_ Z ) -> X C_ A )
12 1 3 paddss2 
 |-  ( ( K e. HL /\ Y C_ A /\ X C_ A ) -> ( ( Y i^i Z ) C_ Y -> ( X .+ ( Y i^i Z ) ) C_ ( X .+ Y ) ) )
13 9 10 11 12 syl3anc 
 |-  ( ( ( K e. HL /\ ( X C_ A /\ Y C_ A /\ Z e. S ) ) /\ X C_ Z ) -> ( ( Y i^i Z ) C_ Y -> ( X .+ ( Y i^i Z ) ) C_ ( X .+ Y ) ) )
14 8 13 mpi 
 |-  ( ( ( K e. HL /\ ( X C_ A /\ Y C_ A /\ Z e. S ) ) /\ X C_ Z ) -> ( X .+ ( Y i^i Z ) ) C_ ( X .+ Y ) )
15 simpl 
 |-  ( ( K e. HL /\ ( X C_ A /\ Y C_ A /\ Z e. S ) ) -> K e. HL )
16 1 2 psubssat 
 |-  ( ( K e. HL /\ Z e. S ) -> Z C_ A )
17 16 3ad2antr3 
 |-  ( ( K e. HL /\ ( X C_ A /\ Y C_ A /\ Z e. S ) ) -> Z C_ A )
18 simpr2 
 |-  ( ( K e. HL /\ ( X C_ A /\ Y C_ A /\ Z e. S ) ) -> Y C_ A )
19 ssinss1 
 |-  ( Y C_ A -> ( Y i^i Z ) C_ A )
20 18 19 syl 
 |-  ( ( K e. HL /\ ( X C_ A /\ Y C_ A /\ Z e. S ) ) -> ( Y i^i Z ) C_ A )
21 1 3 paddss1 
 |-  ( ( K e. HL /\ Z C_ A /\ ( Y i^i Z ) C_ A ) -> ( X C_ Z -> ( X .+ ( Y i^i Z ) ) C_ ( Z .+ ( Y i^i Z ) ) ) )
22 15 17 20 21 syl3anc 
 |-  ( ( K e. HL /\ ( X C_ A /\ Y C_ A /\ Z e. S ) ) -> ( X C_ Z -> ( X .+ ( Y i^i Z ) ) C_ ( Z .+ ( Y i^i Z ) ) ) )
23 22 imp 
 |-  ( ( ( K e. HL /\ ( X C_ A /\ Y C_ A /\ Z e. S ) ) /\ X C_ Z ) -> ( X .+ ( Y i^i Z ) ) C_ ( Z .+ ( Y i^i Z ) ) )
24 simplr3 
 |-  ( ( ( K e. HL /\ ( X C_ A /\ Y C_ A /\ Z e. S ) ) /\ X C_ Z ) -> Z e. S )
25 9 24 16 syl2anc 
 |-  ( ( ( K e. HL /\ ( X C_ A /\ Y C_ A /\ Z e. S ) ) /\ X C_ Z ) -> Z C_ A )
26 inss2 
 |-  ( Y i^i Z ) C_ Z
27 1 3 paddss2 
 |-  ( ( K e. HL /\ Z C_ A /\ Z C_ A ) -> ( ( Y i^i Z ) C_ Z -> ( Z .+ ( Y i^i Z ) ) C_ ( Z .+ Z ) ) )
28 26 27 mpi 
 |-  ( ( K e. HL /\ Z C_ A /\ Z C_ A ) -> ( Z .+ ( Y i^i Z ) ) C_ ( Z .+ Z ) )
29 9 25 25 28 syl3anc 
 |-  ( ( ( K e. HL /\ ( X C_ A /\ Y C_ A /\ Z e. S ) ) /\ X C_ Z ) -> ( Z .+ ( Y i^i Z ) ) C_ ( Z .+ Z ) )
30 2 3 paddidm 
 |-  ( ( K e. HL /\ Z e. S ) -> ( Z .+ Z ) = Z )
31 9 24 30 syl2anc 
 |-  ( ( ( K e. HL /\ ( X C_ A /\ Y C_ A /\ Z e. S ) ) /\ X C_ Z ) -> ( Z .+ Z ) = Z )
32 29 31 sseqtrd 
 |-  ( ( ( K e. HL /\ ( X C_ A /\ Y C_ A /\ Z e. S ) ) /\ X C_ Z ) -> ( Z .+ ( Y i^i Z ) ) C_ Z )
33 23 32 sstrd 
 |-  ( ( ( K e. HL /\ ( X C_ A /\ Y C_ A /\ Z e. S ) ) /\ X C_ Z ) -> ( X .+ ( Y i^i Z ) ) C_ Z )
34 14 33 ssind 
 |-  ( ( ( 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 ) )
35 7 34 eqssd 
 |-  ( ( ( K e. HL /\ ( X C_ A /\ Y C_ A /\ Z e. S ) ) /\ X C_ Z ) -> ( ( X .+ Y ) i^i Z ) = ( X .+ ( Y i^i Z ) ) )
36 35 ex 
 |-  ( ( K e. HL /\ ( X C_ A /\ Y C_ A /\ Z e. S ) ) -> ( X C_ Z -> ( ( X .+ Y ) i^i Z ) = ( X .+ ( Y i^i Z ) ) ) )