Metamath Proof Explorer

Theorem pmapjat2

Description: The projective map of the join of an atom with a lattice element. (Contributed by NM, 12-May-2012)

Ref Expression
Hypotheses pmapjat.b ⊢ B = Base K
pmapjat.j ⊢ ∨ ˙ = join ⁡ K
pmapjat.a ⊢ A = Atoms ⁡ K
pmapjat.m ⊢ M = pmap ⁡ K
pmapjat.p ⊢ + ˙ = + 𝑃 ⁡ K
Assertion pmapjat2 ⊢ K ∈ HL ∧ X ∈ B ∧ Q ∈ A → M ⁡ Q ∨ ˙ X = M ⁡ Q + ˙ M ⁡ X

Proof

Step Hyp Ref Expression
1 pmapjat.b ⊢ B = Base K
2 pmapjat.j ⊢ ∨ ˙ = join ⁡ K
3 pmapjat.a ⊢ A = Atoms ⁡ K
4 pmapjat.m ⊢ M = pmap ⁡ K
5 pmapjat.p ⊢ + ˙ = + 𝑃 ⁡ K
6 1 2 3 4 5 pmapjat1 ⊢ K ∈ HL ∧ X ∈ B ∧ Q ∈ A → M ⁡ X ∨ ˙ Q = M ⁡ X + ˙ M ⁡ Q
7 hllat ⊢ K ∈ HL → K ∈ Lat
8 7 3ad2ant1 ⊢ K ∈ HL ∧ X ∈ B ∧ Q ∈ A → K ∈ Lat
9 1 3 atbase ⊢ Q ∈ A → Q ∈ B
10 9 3ad2ant3 ⊢ K ∈ HL ∧ X ∈ B ∧ Q ∈ A → Q ∈ B
11 simp2 ⊢ K ∈ HL ∧ X ∈ B ∧ Q ∈ A → X ∈ B
12 1 2 latjcom ⊢ K ∈ Lat ∧ Q ∈ B ∧ X ∈ B → Q ∨ ˙ X = X ∨ ˙ Q
13 8 10 11 12 syl3anc ⊢ K ∈ HL ∧ X ∈ B ∧ Q ∈ A → Q ∨ ˙ X = X ∨ ˙ Q
14 13 fveq2d ⊢ K ∈ HL ∧ X ∈ B ∧ Q ∈ A → M ⁡ Q ∨ ˙ X = M ⁡ X ∨ ˙ Q
15 simp1 ⊢ K ∈ HL ∧ X ∈ B ∧ Q ∈ A → K ∈ HL
16 1 3 4 pmapssat ⊢ K ∈ HL ∧ Q ∈ B → M ⁡ Q ⊆ A
17 15 10 16 syl2anc ⊢ K ∈ HL ∧ X ∈ B ∧ Q ∈ A → M ⁡ Q ⊆ A
18 1 3 4 pmapssat ⊢ K ∈ HL ∧ X ∈ B → M ⁡ X ⊆ A
19 18 3adant3 ⊢ K ∈ HL ∧ X ∈ B ∧ Q ∈ A → M ⁡ X ⊆ A
20 3 5 paddcom ⊢ K ∈ Lat ∧ M ⁡ Q ⊆ A ∧ M ⁡ X ⊆ A → M ⁡ Q + ˙ M ⁡ X = M ⁡ X + ˙ M ⁡ Q
21 8 17 19 20 syl3anc ⊢ K ∈ HL ∧ X ∈ B ∧ Q ∈ A → M ⁡ Q + ˙ M ⁡ X = M ⁡ X + ˙ M ⁡ Q
22 6 14 21 3eqtr4d ⊢ K ∈ HL ∧ X ∈ B ∧ Q ∈ A → M ⁡ Q ∨ ˙ X = M ⁡ Q + ˙ M ⁡ X