Metamath Proof Explorer

Theorem pmodN

Description: The modular law for projective subspaces. (Contributed by NM, 26-Mar-2012) (New usage is discouraged.)

Ref Expression
Hypotheses pmod.a 
|- A = ( Atoms ` K )
pmod.s 
|- S = ( PSubSp ` K )
pmod.p 
|- .+ = ( +P ` K )
Assertion pmodN 
|- ( ( K e. HL /\ ( X e. S /\ Y C_ A /\ Z C_ A ) ) -> ( X i^i ( Y .+ ( X i^i Z ) ) ) = ( ( X i^i Y ) .+ ( X 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 incom 
 |-  ( X i^i ( ( X i^i Z ) .+ Y ) ) = ( ( ( X i^i Z ) .+ Y ) i^i X )
5 hllat 
 |-  ( K e. HL -> K e. Lat )
6 5 adantr 
 |-  ( ( K e. HL /\ ( X e. S /\ Y C_ A /\ Z C_ A ) ) -> K e. Lat )
7 simpr2 
 |-  ( ( K e. HL /\ ( X e. S /\ Y C_ A /\ Z C_ A ) ) -> Y C_ A )
8 inss2 
 |-  ( X i^i Z ) C_ Z
9 simpr3 
 |-  ( ( K e. HL /\ ( X e. S /\ Y C_ A /\ Z C_ A ) ) -> Z C_ A )
10 8 9 sstrid 
 |-  ( ( K e. HL /\ ( X e. S /\ Y C_ A /\ Z C_ A ) ) -> ( X i^i Z ) C_ A )
11 1 3 paddcom 
 |-  ( ( K e. Lat /\ Y C_ A /\ ( X i^i Z ) C_ A ) -> ( Y .+ ( X i^i Z ) ) = ( ( X i^i Z ) .+ Y ) )
12 6 7 10 11 syl3anc 
 |-  ( ( K e. HL /\ ( X e. S /\ Y C_ A /\ Z C_ A ) ) -> ( Y .+ ( X i^i Z ) ) = ( ( X i^i Z ) .+ Y ) )
13 12 ineq2d 
 |-  ( ( K e. HL /\ ( X e. S /\ Y C_ A /\ Z C_ A ) ) -> ( X i^i ( Y .+ ( X i^i Z ) ) ) = ( X i^i ( ( X i^i Z ) .+ Y ) ) )
14 incom 
 |-  ( X i^i Y ) = ( Y i^i X )
15 14 oveq2i 
 |-  ( ( X i^i Z ) .+ ( X i^i Y ) ) = ( ( X i^i Z ) .+ ( Y i^i X ) )
16 inss2 
 |-  ( X i^i Y ) C_ Y
17 16 7 sstrid 
 |-  ( ( K e. HL /\ ( X e. S /\ Y C_ A /\ Z C_ A ) ) -> ( X i^i Y ) C_ A )
18 1 3 paddcom 
 |-  ( ( K e. Lat /\ ( X i^i Y ) C_ A /\ ( X i^i Z ) C_ A ) -> ( ( X i^i Y ) .+ ( X i^i Z ) ) = ( ( X i^i Z ) .+ ( X i^i Y ) ) )
19 6 17 10 18 syl3anc 
 |-  ( ( K e. HL /\ ( X e. S /\ Y C_ A /\ Z C_ A ) ) -> ( ( X i^i Y ) .+ ( X i^i Z ) ) = ( ( X i^i Z ) .+ ( X i^i Y ) ) )
20 simpr1 
 |-  ( ( K e. HL /\ ( X e. S /\ Y C_ A /\ Z C_ A ) ) -> X e. S )
21 10 7 20 3jca 
 |-  ( ( K e. HL /\ ( X e. S /\ Y C_ A /\ Z C_ A ) ) -> ( ( X i^i Z ) C_ A /\ Y C_ A /\ X e. S ) )
22 inss1 
 |-  ( X i^i Z ) C_ X
23 1 2 3 pmod1i 
 |-  ( ( K e. HL /\ ( ( X i^i Z ) C_ A /\ Y C_ A /\ X e. S ) ) -> ( ( X i^i Z ) C_ X -> ( ( ( X i^i Z ) .+ Y ) i^i X ) = ( ( X i^i Z ) .+ ( Y i^i X ) ) ) )
24 22 23 mpi 
 |-  ( ( K e. HL /\ ( ( X i^i Z ) C_ A /\ Y C_ A /\ X e. S ) ) -> ( ( ( X i^i Z ) .+ Y ) i^i X ) = ( ( X i^i Z ) .+ ( Y i^i X ) ) )
25 21 24 syldan 
 |-  ( ( K e. HL /\ ( X e. S /\ Y C_ A /\ Z C_ A ) ) -> ( ( ( X i^i Z ) .+ Y ) i^i X ) = ( ( X i^i Z ) .+ ( Y i^i X ) ) )
26 15 19 25 3eqtr4a 
 |-  ( ( K e. HL /\ ( X e. S /\ Y C_ A /\ Z C_ A ) ) -> ( ( X i^i Y ) .+ ( X i^i Z ) ) = ( ( ( X i^i Z ) .+ Y ) i^i X ) )
27 4 13 26 3eqtr4a 
 |-  ( ( K e. HL /\ ( X e. S /\ Y C_ A /\ Z C_ A ) ) -> ( X i^i ( Y .+ ( X i^i Z ) ) ) = ( ( X i^i Y ) .+ ( X i^i Z ) ) )