Metamath Proof Explorer

Theorem dihjust

Description: Part of proof after Lemma N of Crawley p. 122 line 4, "the definition of phi(x) is independent of the atom q." (Contributed by NM, 2-Mar-2014)

Ref Expression
Hypotheses dihjust.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
dihjust.l ⊢ ≤ = ( le ‘ 𝐾 )
dihjust.j ⊢ ∨ = ( join ‘ 𝐾 )
dihjust.m ⊢ ∧ = ( meet ‘ 𝐾 )
dihjust.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
dihjust.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
dihjust.i ⊢ 𝐼 = ( ( DIsoB ‘ 𝐾 ) ‘ 𝑊 )
dihjust.J ⊢ 𝐽 = ( ( DIsoC ‘ 𝐾 ) ‘ 𝑊 )
dihjust.u ⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
dihjust.s ⊢ ⊕ = ( LSSum ‘ 𝑈 )
Assertion dihjust ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑄 ∨ ( 𝑋 ∧ 𝑊 ) ) = ( 𝑅 ∨ ( 𝑋 ∧ 𝑊 ) ) ) → ( ( 𝐽 ‘ 𝑄 ) ⊕ ( 𝐼 ‘ ( 𝑋 ∧ 𝑊 ) ) ) = ( ( 𝐽 ‘ 𝑅 ) ⊕ ( 𝐼 ‘ ( 𝑋 ∧ 𝑊 ) ) ) )

Proof

Step Hyp Ref Expression
1 dihjust.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
2 dihjust.l ⊢ ≤ = ( le ‘ 𝐾 )
3 dihjust.j ⊢ ∨ = ( join ‘ 𝐾 )
4 dihjust.m ⊢ ∧ = ( meet ‘ 𝐾 )
5 dihjust.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
6 dihjust.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
7 dihjust.i ⊢ 𝐼 = ( ( DIsoB ‘ 𝐾 ) ‘ 𝑊 )
8 dihjust.J ⊢ 𝐽 = ( ( DIsoC ‘ 𝐾 ) ‘ 𝑊 )
9 dihjust.u ⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
10 dihjust.s ⊢ ⊕ = ( LSSum ‘ 𝑈 )
11 1 2 3 4 5 6 7 8 9 10 dihjustlem ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑄 ∨ ( 𝑋 ∧ 𝑊 ) ) = ( 𝑅 ∨ ( 𝑋 ∧ 𝑊 ) ) ) → ( ( 𝐽 ‘ 𝑄 ) ⊕ ( 𝐼 ‘ ( 𝑋 ∧ 𝑊 ) ) ) ⊆ ( ( 𝐽 ‘ 𝑅 ) ⊕ ( 𝐼 ‘ ( 𝑋 ∧ 𝑊 ) ) ) )
12 simp1 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑄 ∨ ( 𝑋 ∧ 𝑊 ) ) = ( 𝑅 ∨ ( 𝑋 ∧ 𝑊 ) ) ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
13 simp22 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑄 ∨ ( 𝑋 ∧ 𝑊 ) ) = ( 𝑅 ∨ ( 𝑋 ∧ 𝑊 ) ) ) → ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) )
14 simp21 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑄 ∨ ( 𝑋 ∧ 𝑊 ) ) = ( 𝑅 ∨ ( 𝑋 ∧ 𝑊 ) ) ) → ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) )
15 simp23 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑄 ∨ ( 𝑋 ∧ 𝑊 ) ) = ( 𝑅 ∨ ( 𝑋 ∧ 𝑊 ) ) ) → 𝑋 ∈ 𝐵 )
16 simp3 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑄 ∨ ( 𝑋 ∧ 𝑊 ) ) = ( 𝑅 ∨ ( 𝑋 ∧ 𝑊 ) ) ) → ( 𝑄 ∨ ( 𝑋 ∧ 𝑊 ) ) = ( 𝑅 ∨ ( 𝑋 ∧ 𝑊 ) ) )
17 16 eqcomd ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑄 ∨ ( 𝑋 ∧ 𝑊 ) ) = ( 𝑅 ∨ ( 𝑋 ∧ 𝑊 ) ) ) → ( 𝑅 ∨ ( 𝑋 ∧ 𝑊 ) ) = ( 𝑄 ∨ ( 𝑋 ∧ 𝑊 ) ) )
18 1 2 3 4 5 6 7 8 9 10 dihjustlem ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑅 ∨ ( 𝑋 ∧ 𝑊 ) ) = ( 𝑄 ∨ ( 𝑋 ∧ 𝑊 ) ) ) → ( ( 𝐽 ‘ 𝑅 ) ⊕ ( 𝐼 ‘ ( 𝑋 ∧ 𝑊 ) ) ) ⊆ ( ( 𝐽 ‘ 𝑄 ) ⊕ ( 𝐼 ‘ ( 𝑋 ∧ 𝑊 ) ) ) )
19 12 13 14 15 17 18 syl131anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑄 ∨ ( 𝑋 ∧ 𝑊 ) ) = ( 𝑅 ∨ ( 𝑋 ∧ 𝑊 ) ) ) → ( ( 𝐽 ‘ 𝑅 ) ⊕ ( 𝐼 ‘ ( 𝑋 ∧ 𝑊 ) ) ) ⊆ ( ( 𝐽 ‘ 𝑄 ) ⊕ ( 𝐼 ‘ ( 𝑋 ∧ 𝑊 ) ) ) )
20 11 19 eqssd ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑄 ∨ ( 𝑋 ∧ 𝑊 ) ) = ( 𝑅 ∨ ( 𝑋 ∧ 𝑊 ) ) ) → ( ( 𝐽 ‘ 𝑄 ) ⊕ ( 𝐼 ‘ ( 𝑋 ∧ 𝑊 ) ) ) = ( ( 𝐽 ‘ 𝑅 ) ⊕ ( 𝐼 ‘ ( 𝑋 ∧ 𝑊 ) ) ) )