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

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 ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
pmod.s ⊢ 𝑆 = ( PSubSp ‘ 𝐾 )
pmod.p ⊢ + = ( +𝑃 ‘ 𝐾 )
Assertion pmod2iN ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝑆 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴 ) ) → ( 𝑍 ⊆ 𝑋 → ( ( 𝑋 ∩ 𝑌 ) + 𝑍 ) = ( 𝑋 ∩ ( 𝑌 + 𝑍 ) ) ) )

Proof

Step Hyp Ref Expression
1 pmod.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
2 pmod.s ⊢ 𝑆 = ( PSubSp ‘ 𝐾 )
3 pmod.p ⊢ + = ( +𝑃 ‘ 𝐾 )
4 incom ⊢ ( 𝑋 ∩ 𝑌 ) = ( 𝑌 ∩ 𝑋 )
5 4 oveq1i ⊢ ( ( 𝑋 ∩ 𝑌 ) + 𝑍 ) = ( ( 𝑌 ∩ 𝑋 ) + 𝑍 )
6 hllat ⊢ ( 𝐾 ∈ HL → 𝐾 ∈ Lat )
7 6 3ad2ant1 ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝑆 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴 ) ∧ 𝑍 ⊆ 𝑋 ) → 𝐾 ∈ Lat )
8 simp22 ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝑆 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴 ) ∧ 𝑍 ⊆ 𝑋 ) → 𝑌 ⊆ 𝐴 )
9 ssinss1 ⊢ ( 𝑌 ⊆ 𝐴 → ( 𝑌 ∩ 𝑋 ) ⊆ 𝐴 )
10 8 9 syl ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝑆 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴 ) ∧ 𝑍 ⊆ 𝑋 ) → ( 𝑌 ∩ 𝑋 ) ⊆ 𝐴 )
11 simp23 ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝑆 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴 ) ∧ 𝑍 ⊆ 𝑋 ) → 𝑍 ⊆ 𝐴 )
12 1 3 paddcom ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑌 ∩ 𝑋 ) ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴 ) → ( ( 𝑌 ∩ 𝑋 ) + 𝑍 ) = ( 𝑍 + ( 𝑌 ∩ 𝑋 ) ) )
13 7 10 11 12 syl3anc ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝑆 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴 ) ∧ 𝑍 ⊆ 𝑋 ) → ( ( 𝑌 ∩ 𝑋 ) + 𝑍 ) = ( 𝑍 + ( 𝑌 ∩ 𝑋 ) ) )
14 5 13 eqtrid ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝑆 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴 ) ∧ 𝑍 ⊆ 𝑋 ) → ( ( 𝑋 ∩ 𝑌 ) + 𝑍 ) = ( 𝑍 + ( 𝑌 ∩ 𝑋 ) ) )
15 simp21 ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝑆 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴 ) ∧ 𝑍 ⊆ 𝑋 ) → 𝑋 ∈ 𝑆 )
16 11 8 15 3jca ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝑆 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴 ) ∧ 𝑍 ⊆ 𝑋 ) → ( 𝑍 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑋 ∈ 𝑆 ) )
17 1 2 3 pmod1i ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑍 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑋 ∈ 𝑆 ) ) → ( 𝑍 ⊆ 𝑋 → ( ( 𝑍 + 𝑌 ) ∩ 𝑋 ) = ( 𝑍 + ( 𝑌 ∩ 𝑋 ) ) ) )
18 17 3impia ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑍 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑋 ∈ 𝑆 ) ∧ 𝑍 ⊆ 𝑋 ) → ( ( 𝑍 + 𝑌 ) ∩ 𝑋 ) = ( 𝑍 + ( 𝑌 ∩ 𝑋 ) ) )
19 16 18 syld3an2 ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝑆 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴 ) ∧ 𝑍 ⊆ 𝑋 ) → ( ( 𝑍 + 𝑌 ) ∩ 𝑋 ) = ( 𝑍 + ( 𝑌 ∩ 𝑋 ) ) )
20 1 3 paddcom ⊢ ( ( 𝐾 ∈ Lat ∧ 𝑍 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ) → ( 𝑍 + 𝑌 ) = ( 𝑌 + 𝑍 ) )
21 7 11 8 20 syl3anc ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝑆 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴 ) ∧ 𝑍 ⊆ 𝑋 ) → ( 𝑍 + 𝑌 ) = ( 𝑌 + 𝑍 ) )
22 21 ineq1d ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝑆 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴 ) ∧ 𝑍 ⊆ 𝑋 ) → ( ( 𝑍 + 𝑌 ) ∩ 𝑋 ) = ( ( 𝑌 + 𝑍 ) ∩ 𝑋 ) )
23 14 19 22 3eqtr2d ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝑆 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴 ) ∧ 𝑍 ⊆ 𝑋 ) → ( ( 𝑋 ∩ 𝑌 ) + 𝑍 ) = ( ( 𝑌 + 𝑍 ) ∩ 𝑋 ) )
24 incom ⊢ ( ( 𝑌 + 𝑍 ) ∩ 𝑋 ) = ( 𝑋 ∩ ( 𝑌 + 𝑍 ) )
25 23 24 eqtrdi ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝑆 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴 ) ∧ 𝑍 ⊆ 𝑋 ) → ( ( 𝑋 ∩ 𝑌 ) + 𝑍 ) = ( 𝑋 ∩ ( 𝑌 + 𝑍 ) ) )
26 25 3expia ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝑆 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴 ) ) → ( 𝑍 ⊆ 𝑋 → ( ( 𝑋 ∩ 𝑌 ) + 𝑍 ) = ( 𝑋 ∩ ( 𝑌 + 𝑍 ) ) ) )