Metamath Proof Explorer

Theorem paddval

Description: Projective subspace sum operation value. (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 paddval ⊢ K ∈ B ∧ X ⊆ A ∧ Y ⊆ A → X + ˙ Y = X ∪ Y ∪ p ∈ A | ∃ q ∈ X ∃ r ∈ Y 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 biid ⊢ K ∈ B ↔ K ∈ B
6 3 fvexi ⊢ A ∈ V
7 6 elpw2 ⊢ X ∈ 𝒫 A ↔ X ⊆ A
8 6 elpw2 ⊢ Y ∈ 𝒫 A ↔ Y ⊆ A
9 1 2 3 4 paddfval ⊢ K ∈ B → + ˙ = m ∈ 𝒫 A , n ∈ 𝒫 A ⟼ m ∪ n ∪ p ∈ A | ∃ q ∈ m ∃ r ∈ n p ≤ ˙ q ∨ ˙ r
10 9 oveqd ⊢ K ∈ B → X + ˙ Y = X m ∈ 𝒫 A , n ∈ 𝒫 A ⟼ m ∪ n ∪ p ∈ A | ∃ q ∈ m ∃ r ∈ n p ≤ ˙ q ∨ ˙ r Y
11 10 3ad2ant1 ⊢ K ∈ B ∧ X ∈ 𝒫 A ∧ Y ∈ 𝒫 A → X + ˙ Y = X m ∈ 𝒫 A , n ∈ 𝒫 A ⟼ m ∪ n ∪ p ∈ A | ∃ q ∈ m ∃ r ∈ n p ≤ ˙ q ∨ ˙ r Y
12 simpl ⊢ X ∈ 𝒫 A ∧ Y ∈ 𝒫 A → X ∈ 𝒫 A
13 simpr ⊢ X ∈ 𝒫 A ∧ Y ∈ 𝒫 A → Y ∈ 𝒫 A
14 unexg ⊢ X ∈ 𝒫 A ∧ Y ∈ 𝒫 A → X ∪ Y ∈ V
15 6 rabex ⊢ p ∈ A | ∃ q ∈ X ∃ r ∈ Y p ≤ ˙ q ∨ ˙ r ∈ V
16 unexg ⊢ X ∪ Y ∈ V ∧ p ∈ A | ∃ q ∈ X ∃ r ∈ Y p ≤ ˙ q ∨ ˙ r ∈ V → X ∪ Y ∪ p ∈ A | ∃ q ∈ X ∃ r ∈ Y p ≤ ˙ q ∨ ˙ r ∈ V
17 14 15 16 sylancl ⊢ X ∈ 𝒫 A ∧ Y ∈ 𝒫 A → X ∪ Y ∪ p ∈ A | ∃ q ∈ X ∃ r ∈ Y p ≤ ˙ q ∨ ˙ r ∈ V
18 12 13 17 3jca ⊢ X ∈ 𝒫 A ∧ Y ∈ 𝒫 A → X ∈ 𝒫 A ∧ Y ∈ 𝒫 A ∧ X ∪ Y ∪ p ∈ A | ∃ q ∈ X ∃ r ∈ Y p ≤ ˙ q ∨ ˙ r ∈ V
19 18 3adant1 ⊢ K ∈ B ∧ X ∈ 𝒫 A ∧ Y ∈ 𝒫 A → X ∈ 𝒫 A ∧ Y ∈ 𝒫 A ∧ X ∪ Y ∪ p ∈ A | ∃ q ∈ X ∃ r ∈ Y p ≤ ˙ q ∨ ˙ r ∈ V
20 uneq1 ⊢ m = X → m ∪ n = X ∪ n
21 rexeq ⊢ m = X → ∃ q ∈ m ∃ r ∈ n p ≤ ˙ q ∨ ˙ r ↔ ∃ q ∈ X ∃ r ∈ n p ≤ ˙ q ∨ ˙ r
22 21 rabbidv ⊢ m = X → p ∈ A | ∃ q ∈ m ∃ r ∈ n p ≤ ˙ q ∨ ˙ r = p ∈ A | ∃ q ∈ X ∃ r ∈ n p ≤ ˙ q ∨ ˙ r
23 20 22 uneq12d ⊢ m = X → m ∪ n ∪ p ∈ A | ∃ q ∈ m ∃ r ∈ n p ≤ ˙ q ∨ ˙ r = X ∪ n ∪ p ∈ A | ∃ q ∈ X ∃ r ∈ n p ≤ ˙ q ∨ ˙ r
24 uneq2 ⊢ n = Y → X ∪ n = X ∪ Y
25 rexeq ⊢ n = Y → ∃ r ∈ n p ≤ ˙ q ∨ ˙ r ↔ ∃ r ∈ Y p ≤ ˙ q ∨ ˙ r
26 25 rexbidv ⊢ n = Y → ∃ q ∈ X ∃ r ∈ n p ≤ ˙ q ∨ ˙ r ↔ ∃ q ∈ X ∃ r ∈ Y p ≤ ˙ q ∨ ˙ r
27 26 rabbidv ⊢ n = Y → p ∈ A | ∃ q ∈ X ∃ r ∈ n p ≤ ˙ q ∨ ˙ r = p ∈ A | ∃ q ∈ X ∃ r ∈ Y p ≤ ˙ q ∨ ˙ r
28 24 27 uneq12d ⊢ n = Y → X ∪ n ∪ p ∈ A | ∃ q ∈ X ∃ r ∈ n p ≤ ˙ q ∨ ˙ r = X ∪ Y ∪ p ∈ A | ∃ q ∈ X ∃ r ∈ Y p ≤ ˙ q ∨ ˙ r
29 eqid ⊢ m ∈ 𝒫 A , n ∈ 𝒫 A ⟼ m ∪ n ∪ p ∈ A | ∃ q ∈ m ∃ r ∈ n p ≤ ˙ q ∨ ˙ r = m ∈ 𝒫 A , n ∈ 𝒫 A ⟼ m ∪ n ∪ p ∈ A | ∃ q ∈ m ∃ r ∈ n p ≤ ˙ q ∨ ˙ r
30 23 28 29 ovmpog ⊢ X ∈ 𝒫 A ∧ Y ∈ 𝒫 A ∧ X ∪ Y ∪ p ∈ A | ∃ q ∈ X ∃ r ∈ Y p ≤ ˙ q ∨ ˙ r ∈ V → X m ∈ 𝒫 A , n ∈ 𝒫 A ⟼ m ∪ n ∪ p ∈ A | ∃ q ∈ m ∃ r ∈ n p ≤ ˙ q ∨ ˙ r Y = X ∪ Y ∪ p ∈ A | ∃ q ∈ X ∃ r ∈ Y p ≤ ˙ q ∨ ˙ r
31 19 30 syl ⊢ K ∈ B ∧ X ∈ 𝒫 A ∧ Y ∈ 𝒫 A → X m ∈ 𝒫 A , n ∈ 𝒫 A ⟼ m ∪ n ∪ p ∈ A | ∃ q ∈ m ∃ r ∈ n p ≤ ˙ q ∨ ˙ r Y = X ∪ Y ∪ p ∈ A | ∃ q ∈ X ∃ r ∈ Y p ≤ ˙ q ∨ ˙ r
32 11 31 eqtrd ⊢ K ∈ B ∧ X ∈ 𝒫 A ∧ Y ∈ 𝒫 A → X + ˙ Y = X ∪ Y ∪ p ∈ A | ∃ q ∈ X ∃ r ∈ Y p ≤ ˙ q ∨ ˙ r
33 5 7 8 32 syl3anbr ⊢ K ∈ B ∧ X ⊆ A ∧ Y ⊆ A → X + ˙ Y = X ∪ Y ∪ p ∈ A | ∃ q ∈ X ∃ r ∈ Y p ≤ ˙ q ∨ ˙ r