Metamath Proof Explorer

Theorem paddfval

Description: Projective subspace sum operation. (Contributed by NM, 29-Dec-2011)

Ref Expression
Hypotheses paddfval.l ⊢ ≤ ˙ = ≤ K
paddfval.j ⊢ ∨ ˙ = join ⁡ K
paddfval.a ⊢ A = Atoms ⁡ K
paddfval.p ⊢ + ˙ = + 𝑃 ⁡ K
Assertion paddfval ⊢ K ∈ B → + ˙ = m ∈ 𝒫 A , n ∈ 𝒫 A ⟼ m ∪ n ∪ p ∈ A | ∃ q ∈ m ∃ r ∈ n p ≤ ˙ q ∨ ˙ r

Proof

Step Hyp Ref Expression
1 paddfval.l ⊢ ≤ ˙ = ≤ K
2 paddfval.j ⊢ ∨ ˙ = join ⁡ K
3 paddfval.a ⊢ A = Atoms ⁡ K
4 paddfval.p ⊢ + ˙ = + 𝑃 ⁡ K
5 elex ⊢ K ∈ B → K ∈ V
6 fveq2 ⊢ h = K → Atoms ⁡ h = Atoms ⁡ K
7 6 3 eqtr4di ⊢ h = K → Atoms ⁡ h = A
8 7 pweqd ⊢ h = K → 𝒫 Atoms ⁡ h = 𝒫 A
9 eqidd ⊢ h = K → p = p
10 fveq2 ⊢ h = K → ≤ h = ≤ K
11 10 1 eqtr4di ⊢ h = K → ≤ h = ≤ ˙
12 fveq2 ⊢ h = K → join ⁡ h = join ⁡ K
13 12 2 eqtr4di ⊢ h = K → join ⁡ h = ∨ ˙
14 13 oveqd ⊢ h = K → q join ⁡ h r = q ∨ ˙ r
15 9 11 14 breq123d ⊢ h = K → p ≤ h q join ⁡ h r ↔ p ≤ ˙ q ∨ ˙ r
16 15 2rexbidv ⊢ h = K → ∃ q ∈ m ∃ r ∈ n p ≤ h q join ⁡ h r ↔ ∃ q ∈ m ∃ r ∈ n p ≤ ˙ q ∨ ˙ r
17 7 16 rabeqbidv ⊢ h = K → p ∈ Atoms ⁡ h | ∃ q ∈ m ∃ r ∈ n p ≤ h q join ⁡ h r = p ∈ A | ∃ q ∈ m ∃ r ∈ n p ≤ ˙ q ∨ ˙ r
18 17 uneq2d ⊢ h = K → m ∪ n ∪ p ∈ Atoms ⁡ h | ∃ q ∈ m ∃ r ∈ n p ≤ h q join ⁡ h r = m ∪ n ∪ p ∈ A | ∃ q ∈ m ∃ r ∈ n p ≤ ˙ q ∨ ˙ r
19 8 8 18 mpoeq123dv ⊢ h = K → m ∈ 𝒫 Atoms ⁡ h , n ∈ 𝒫 Atoms ⁡ h ⟼ m ∪ n ∪ p ∈ Atoms ⁡ h | ∃ q ∈ m ∃ r ∈ n p ≤ h q join ⁡ h r = m ∈ 𝒫 A , n ∈ 𝒫 A ⟼ m ∪ n ∪ p ∈ A | ∃ q ∈ m ∃ r ∈ n p ≤ ˙ q ∨ ˙ r
20 df-padd ⊢ + 𝑃 = h ∈ V ⟼ m ∈ 𝒫 Atoms ⁡ h , n ∈ 𝒫 Atoms ⁡ h ⟼ m ∪ n ∪ p ∈ Atoms ⁡ h | ∃ q ∈ m ∃ r ∈ n p ≤ h q join ⁡ h r
21 3 fvexi ⊢ A ∈ V
22 21 pwex ⊢ 𝒫 A ∈ V
23 22 22 mpoex ⊢ m ∈ 𝒫 A , n ∈ 𝒫 A ⟼ m ∪ n ∪ p ∈ A | ∃ q ∈ m ∃ r ∈ n p ≤ ˙ q ∨ ˙ r ∈ V
24 19 20 23 fvmpt ⊢ K ∈ V → + 𝑃 ⁡ K = m ∈ 𝒫 A , n ∈ 𝒫 A ⟼ m ∪ n ∪ p ∈ A | ∃ q ∈ m ∃ r ∈ n p ≤ ˙ q ∨ ˙ r
25 4 24 syl5eq ⊢ K ∈ V → + ˙ = m ∈ 𝒫 A , n ∈ 𝒫 A ⟼ m ∪ n ∪ p ∈ A | ∃ q ∈ m ∃ r ∈ n p ≤ ˙ q ∨ ˙ r
26 5 25 syl ⊢ K ∈ B → + ˙ = m ∈ 𝒫 A , n ∈ 𝒫 A ⟼ m ∪ n ∪ p ∈ A | ∃ q ∈ m ∃ r ∈ n p ≤ ˙ q ∨ ˙ r