Metamath Proof Explorer

Theorem pmod2iN

Description: Dual of the modular law. (Contributed by NM, 8-Apr-2012) (New usage is discouraged.)

Ref Expression
Hypotheses pmod.a 
|- A = ( Atoms ` K )
pmod.s 
|- S = ( PSubSp ` K )
pmod.p 
|- .+ = ( +P ` K )
Assertion pmod2iN 
|- ( ( K e. HL /\ ( X e. S /\ Y C_ A /\ Z C_ A ) ) -> ( Z C_ X -> ( ( X i^i Y ) .+ Z ) = ( X i^i ( Y .+ 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 Y ) = ( Y i^i X )
5 4 oveq1i 
 |-  ( ( X i^i Y ) .+ Z ) = ( ( Y i^i X ) .+ Z )
6 hllat 
 |-  ( K e. HL -> K e. Lat )
7 6 3ad2ant1 
 |-  ( ( K e. HL /\ ( X e. S /\ Y C_ A /\ Z C_ A ) /\ Z C_ X ) -> K e. Lat )
8 simp22 
 |-  ( ( K e. HL /\ ( X e. S /\ Y C_ A /\ Z C_ A ) /\ Z C_ X ) -> Y C_ A )
9 ssinss1 
 |-  ( Y C_ A -> ( Y i^i X ) C_ A )
10 8 9 syl 
 |-  ( ( K e. HL /\ ( X e. S /\ Y C_ A /\ Z C_ A ) /\ Z C_ X ) -> ( Y i^i X ) C_ A )
11 simp23 
 |-  ( ( K e. HL /\ ( X e. S /\ Y C_ A /\ Z C_ A ) /\ Z C_ X ) -> Z C_ A )
12 1 3 paddcom 
 |-  ( ( K e. Lat /\ ( Y i^i X ) C_ A /\ Z C_ A ) -> ( ( Y i^i X ) .+ Z ) = ( Z .+ ( Y i^i X ) ) )
13 7 10 11 12 syl3anc 
 |-  ( ( K e. HL /\ ( X e. S /\ Y C_ A /\ Z C_ A ) /\ Z C_ X ) -> ( ( Y i^i X ) .+ Z ) = ( Z .+ ( Y i^i X ) ) )
14 5 13 syl5eq 
 |-  ( ( K e. HL /\ ( X e. S /\ Y C_ A /\ Z C_ A ) /\ Z C_ X ) -> ( ( X i^i Y ) .+ Z ) = ( Z .+ ( Y i^i X ) ) )
15 simp21 
 |-  ( ( K e. HL /\ ( X e. S /\ Y C_ A /\ Z C_ A ) /\ Z C_ X ) -> X e. S )
16 11 8 15 3jca 
 |-  ( ( K e. HL /\ ( X e. S /\ Y C_ A /\ Z C_ A ) /\ Z C_ X ) -> ( Z C_ A /\ Y C_ A /\ X e. S ) )
17 1 2 3 pmod1i 
 |-  ( ( K e. HL /\ ( Z C_ A /\ Y C_ A /\ X e. S ) ) -> ( Z C_ X -> ( ( Z .+ Y ) i^i X ) = ( Z .+ ( Y i^i X ) ) ) )
18 17 3impia 
 |-  ( ( K e. HL /\ ( Z C_ A /\ Y C_ A /\ X e. S ) /\ Z C_ X ) -> ( ( Z .+ Y ) i^i X ) = ( Z .+ ( Y i^i X ) ) )
19 16 18 syld3an2 
 |-  ( ( K e. HL /\ ( X e. S /\ Y C_ A /\ Z C_ A ) /\ Z C_ X ) -> ( ( Z .+ Y ) i^i X ) = ( Z .+ ( Y i^i X ) ) )
20 1 3 paddcom 
 |-  ( ( K e. Lat /\ Z C_ A /\ Y C_ A ) -> ( Z .+ Y ) = ( Y .+ Z ) )
21 7 11 8 20 syl3anc 
 |-  ( ( K e. HL /\ ( X e. S /\ Y C_ A /\ Z C_ A ) /\ Z C_ X ) -> ( Z .+ Y ) = ( Y .+ Z ) )
22 21 ineq1d 
 |-  ( ( K e. HL /\ ( X e. S /\ Y C_ A /\ Z C_ A ) /\ Z C_ X ) -> ( ( Z .+ Y ) i^i X ) = ( ( Y .+ Z ) i^i X ) )
23 14 19 22 3eqtr2d 
 |-  ( ( K e. HL /\ ( X e. S /\ Y C_ A /\ Z C_ A ) /\ Z C_ X ) -> ( ( X i^i Y ) .+ Z ) = ( ( Y .+ Z ) i^i X ) )
24 incom 
 |-  ( ( Y .+ Z ) i^i X ) = ( X i^i ( Y .+ Z ) )
25 23 24 eqtrdi 
 |-  ( ( K e. HL /\ ( X e. S /\ Y C_ A /\ Z C_ A ) /\ Z C_ X ) -> ( ( X i^i Y ) .+ Z ) = ( X i^i ( Y .+ Z ) ) )
26 25 3expia 
 |-  ( ( K e. HL /\ ( X e. S /\ Y C_ A /\ Z C_ A ) ) -> ( Z C_ X -> ( ( X i^i Y ) .+ Z ) = ( X i^i ( Y .+ Z ) ) ) )