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

Metamath Proof Explorer

Theorem paddval

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

Ref Expression
Hypotheses paddfval.l ⊢ ≤ = ( le ‘ 𝐾 )
paddfval.j ⊢ ∨ = ( join ‘ 𝐾 )
paddfval.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
paddfval.p ⊢ + = ( +𝑃 ‘ 𝐾 )
Assertion paddval ( ( 𝐾 ∈ 𝐵 ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ) → ( 𝑋 + 𝑌 ) = ( ( 𝑋 ∪ 𝑌 ) ∪ { 𝑝 ∈ 𝐴 ∣ ∃ 𝑞 ∈ 𝑋 ∃ 𝑟 ∈ 𝑌 𝑝 ≤ ( 𝑞 ∨ 𝑟 ) } ) )

Proof

Step Hyp Ref Expression
1 paddfval.l ⊢ ≤ = ( le ‘ 𝐾 )
2 paddfval.j ⊢ ∨ = ( join ‘ 𝐾 )
3 paddfval.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
4 paddfval.p ⊢ + = ( +𝑃 ‘ 𝐾 )
5 biid ⊢ ( 𝐾 ∈ 𝐵 ↔ 𝐾 ∈ 𝐵 )
6 3 fvexi ⊢ 𝐴 ∈ V
7 6 elpw2 ⊢ ( 𝑋 ∈ 𝒫 𝐴 ↔ 𝑋 ⊆ 𝐴 )
8 6 elpw2 ⊢ ( 𝑌 ∈ 𝒫 𝐴 ↔ 𝑌 ⊆ 𝐴 )
9 1 2 3 4 paddfval ⊢ ( 𝐾 ∈ 𝐵 → + = ( 𝑚 ∈ 𝒫 𝐴 , 𝑛 ∈ 𝒫 𝐴 ↦ ( ( 𝑚 ∪ 𝑛 ) ∪ { 𝑝 ∈ 𝐴 ∣ ∃ 𝑞 ∈ 𝑚 ∃ 𝑟 ∈ 𝑛 𝑝 ≤ ( 𝑞 ∨ 𝑟 ) } ) ) )
10 9 oveqd ⊢ ( 𝐾 ∈ 𝐵 → ( 𝑋 + 𝑌 ) = ( 𝑋 ( 𝑚 ∈ 𝒫 𝐴 , 𝑛 ∈ 𝒫 𝐴 ↦ ( ( 𝑚 ∪ 𝑛 ) ∪ { 𝑝 ∈ 𝐴 ∣ ∃ 𝑞 ∈ 𝑚 ∃ 𝑟 ∈ 𝑛 𝑝 ≤ ( 𝑞 ∨ 𝑟 ) } ) ) 𝑌 ) )
11 10 3ad2ant1 ⊢ ( ( 𝐾 ∈ 𝐵 ∧ 𝑋 ∈ 𝒫 𝐴 ∧ 𝑌 ∈ 𝒫 𝐴 ) → ( 𝑋 + 𝑌 ) = ( 𝑋 ( 𝑚 ∈ 𝒫 𝐴 , 𝑛 ∈ 𝒫 𝐴 ↦ ( ( 𝑚 ∪ 𝑛 ) ∪ { 𝑝 ∈ 𝐴 ∣ ∃ 𝑞 ∈ 𝑚 ∃ 𝑟 ∈ 𝑛 𝑝 ≤ ( 𝑞 ∨ 𝑟 ) } ) ) 𝑌 ) )
12 simpl ⊢ ( ( 𝑋 ∈ 𝒫 𝐴 ∧ 𝑌 ∈ 𝒫 𝐴 ) → 𝑋 ∈ 𝒫 𝐴 )
13 simpr ⊢ ( ( 𝑋 ∈ 𝒫 𝐴 ∧ 𝑌 ∈ 𝒫 𝐴 ) → 𝑌 ∈ 𝒫 𝐴 )
14 unexg ⊢ ( ( 𝑋 ∈ 𝒫 𝐴 ∧ 𝑌 ∈ 𝒫 𝐴 ) → ( 𝑋 ∪ 𝑌 ) ∈ V )
15 6 rabex ⊢ { 𝑝 ∈ 𝐴 ∣ ∃ 𝑞 ∈ 𝑋 ∃ 𝑟 ∈ 𝑌 𝑝 ≤ ( 𝑞 ∨ 𝑟 ) } ∈ V
16 unexg ⊢ ( ( ( 𝑋 ∪ 𝑌 ) ∈ V ∧ { 𝑝 ∈ 𝐴 ∣ ∃ 𝑞 ∈ 𝑋 ∃ 𝑟 ∈ 𝑌 𝑝 ≤ ( 𝑞 ∨ 𝑟 ) } ∈ V ) → ( ( 𝑋 ∪ 𝑌 ) ∪ { 𝑝 ∈ 𝐴 ∣ ∃ 𝑞 ∈ 𝑋 ∃ 𝑟 ∈ 𝑌 𝑝 ≤ ( 𝑞 ∨ 𝑟 ) } ) ∈ V )
17 14 15 16 sylancl ⊢ ( ( 𝑋 ∈ 𝒫 𝐴 ∧ 𝑌 ∈ 𝒫 𝐴 ) → ( ( 𝑋 ∪ 𝑌 ) ∪ { 𝑝 ∈ 𝐴 ∣ ∃ 𝑞 ∈ 𝑋 ∃ 𝑟 ∈ 𝑌 𝑝 ≤ ( 𝑞 ∨ 𝑟 ) } ) ∈ V )
18 12 13 17 3jca ⊢ ( ( 𝑋 ∈ 𝒫 𝐴 ∧ 𝑌 ∈ 𝒫 𝐴 ) → ( 𝑋 ∈ 𝒫 𝐴 ∧ 𝑌 ∈ 𝒫 𝐴 ∧ ( ( 𝑋 ∪ 𝑌 ) ∪ { 𝑝 ∈ 𝐴 ∣ ∃ 𝑞 ∈ 𝑋 ∃ 𝑟 ∈ 𝑌 𝑝 ≤ ( 𝑞 ∨ 𝑟 ) } ) ∈ V ) )
19 18 3adant1 ⊢ ( ( 𝐾 ∈ 𝐵 ∧ 𝑋 ∈ 𝒫 𝐴 ∧ 𝑌 ∈ 𝒫 𝐴 ) → ( 𝑋 ∈ 𝒫 𝐴 ∧ 𝑌 ∈ 𝒫 𝐴 ∧ ( ( 𝑋 ∪ 𝑌 ) ∪ { 𝑝 ∈ 𝐴 ∣ ∃ 𝑞 ∈ 𝑋 ∃ 𝑟 ∈ 𝑌 𝑝 ≤ ( 𝑞 ∨ 𝑟 ) } ) ∈ V ) )
20 uneq1 ⊢ ( 𝑚 = 𝑋 → ( 𝑚 ∪ 𝑛 ) = ( 𝑋 ∪ 𝑛 ) )
21 rexeq ⊢ ( 𝑚 = 𝑋 → ( ∃ 𝑞 ∈ 𝑚 ∃ 𝑟 ∈ 𝑛 𝑝 ≤ ( 𝑞 ∨ 𝑟 ) ↔ ∃ 𝑞 ∈ 𝑋 ∃ 𝑟 ∈ 𝑛 𝑝 ≤ ( 𝑞 ∨ 𝑟 ) ) )
22 21 rabbidv ⊢ ( 𝑚 = 𝑋 → { 𝑝 ∈ 𝐴 ∣ ∃ 𝑞 ∈ 𝑚 ∃ 𝑟 ∈ 𝑛 𝑝 ≤ ( 𝑞 ∨ 𝑟 ) } = { 𝑝 ∈ 𝐴 ∣ ∃ 𝑞 ∈ 𝑋 ∃ 𝑟 ∈ 𝑛 𝑝 ≤ ( 𝑞 ∨ 𝑟 ) } )
23 20 22 uneq12d ⊢ ( 𝑚 = 𝑋 → ( ( 𝑚 ∪ 𝑛 ) ∪ { 𝑝 ∈ 𝐴 ∣ ∃ 𝑞 ∈ 𝑚 ∃ 𝑟 ∈ 𝑛 𝑝 ≤ ( 𝑞 ∨ 𝑟 ) } ) = ( ( 𝑋 ∪ 𝑛 ) ∪ { 𝑝 ∈ 𝐴 ∣ ∃ 𝑞 ∈ 𝑋 ∃ 𝑟 ∈ 𝑛 𝑝 ≤ ( 𝑞 ∨ 𝑟 ) } ) )
24 uneq2 ⊢ ( 𝑛 = 𝑌 → ( 𝑋 ∪ 𝑛 ) = ( 𝑋 ∪ 𝑌 ) )
25 rexeq ⊢ ( 𝑛 = 𝑌 → ( ∃ 𝑟 ∈ 𝑛 𝑝 ≤ ( 𝑞 ∨ 𝑟 ) ↔ ∃ 𝑟 ∈ 𝑌 𝑝 ≤ ( 𝑞 ∨ 𝑟 ) ) )
26 25 rexbidv ⊢ ( 𝑛 = 𝑌 → ( ∃ 𝑞 ∈ 𝑋 ∃ 𝑟 ∈ 𝑛 𝑝 ≤ ( 𝑞 ∨ 𝑟 ) ↔ ∃ 𝑞 ∈ 𝑋 ∃ 𝑟 ∈ 𝑌 𝑝 ≤ ( 𝑞 ∨ 𝑟 ) ) )
27 26 rabbidv ⊢ ( 𝑛 = 𝑌 → { 𝑝 ∈ 𝐴 ∣ ∃ 𝑞 ∈ 𝑋 ∃ 𝑟 ∈ 𝑛 𝑝 ≤ ( 𝑞 ∨ 𝑟 ) } = { 𝑝 ∈ 𝐴 ∣ ∃ 𝑞 ∈ 𝑋 ∃ 𝑟 ∈ 𝑌 𝑝 ≤ ( 𝑞 ∨ 𝑟 ) } )
28 24 27 uneq12d ⊢ ( 𝑛 = 𝑌 → ( ( 𝑋 ∪ 𝑛 ) ∪ { 𝑝 ∈ 𝐴 ∣ ∃ 𝑞 ∈ 𝑋 ∃ 𝑟 ∈ 𝑛 𝑝 ≤ ( 𝑞 ∨ 𝑟 ) } ) = ( ( 𝑋 ∪ 𝑌 ) ∪ { 𝑝 ∈ 𝐴 ∣ ∃ 𝑞 ∈ 𝑋 ∃ 𝑟 ∈ 𝑌 𝑝 ≤ ( 𝑞 ∨ 𝑟 ) } ) )
29 eqid ⊢ ( 𝑚 ∈ 𝒫 𝐴 , 𝑛 ∈ 𝒫 𝐴 ↦ ( ( 𝑚 ∪ 𝑛 ) ∪ { 𝑝 ∈ 𝐴 ∣ ∃ 𝑞 ∈ 𝑚 ∃ 𝑟 ∈ 𝑛 𝑝 ≤ ( 𝑞 ∨ 𝑟 ) } ) ) = ( 𝑚 ∈ 𝒫 𝐴 , 𝑛 ∈ 𝒫 𝐴 ↦ ( ( 𝑚 ∪ 𝑛 ) ∪ { 𝑝 ∈ 𝐴 ∣ ∃ 𝑞 ∈ 𝑚 ∃ 𝑟 ∈ 𝑛 𝑝 ≤ ( 𝑞 ∨ 𝑟 ) } ) )
30 23 28 29 ovmpog ⊢ ( ( 𝑋 ∈ 𝒫 𝐴 ∧ 𝑌 ∈ 𝒫 𝐴 ∧ ( ( 𝑋 ∪ 𝑌 ) ∪ { 𝑝 ∈ 𝐴 ∣ ∃ 𝑞 ∈ 𝑋 ∃ 𝑟 ∈ 𝑌 𝑝 ≤ ( 𝑞 ∨ 𝑟 ) } ) ∈ V ) → ( 𝑋 ( 𝑚 ∈ 𝒫 𝐴 , 𝑛 ∈ 𝒫 𝐴 ↦ ( ( 𝑚 ∪ 𝑛 ) ∪ { 𝑝 ∈ 𝐴 ∣ ∃ 𝑞 ∈ 𝑚 ∃ 𝑟 ∈ 𝑛 𝑝 ≤ ( 𝑞 ∨ 𝑟 ) } ) ) 𝑌 ) = ( ( 𝑋 ∪ 𝑌 ) ∪ { 𝑝 ∈ 𝐴 ∣ ∃ 𝑞 ∈ 𝑋 ∃ 𝑟 ∈ 𝑌 𝑝 ≤ ( 𝑞 ∨ 𝑟 ) } ) )
31 19 30 syl ⊢ ( ( 𝐾 ∈ 𝐵 ∧ 𝑋 ∈ 𝒫 𝐴 ∧ 𝑌 ∈ 𝒫 𝐴 ) → ( 𝑋 ( 𝑚 ∈ 𝒫 𝐴 , 𝑛 ∈ 𝒫 𝐴 ↦ ( ( 𝑚 ∪ 𝑛 ) ∪ { 𝑝 ∈ 𝐴 ∣ ∃ 𝑞 ∈ 𝑚 ∃ 𝑟 ∈ 𝑛 𝑝 ≤ ( 𝑞 ∨ 𝑟 ) } ) ) 𝑌 ) = ( ( 𝑋 ∪ 𝑌 ) ∪ { 𝑝 ∈ 𝐴 ∣ ∃ 𝑞 ∈ 𝑋 ∃ 𝑟 ∈ 𝑌 𝑝 ≤ ( 𝑞 ∨ 𝑟 ) } ) )
32 11 31 eqtrd ⊢ ( ( 𝐾 ∈ 𝐵 ∧ 𝑋 ∈ 𝒫 𝐴 ∧ 𝑌 ∈ 𝒫 𝐴 ) → ( 𝑋 + 𝑌 ) = ( ( 𝑋 ∪ 𝑌 ) ∪ { 𝑝 ∈ 𝐴 ∣ ∃ 𝑞 ∈ 𝑋 ∃ 𝑟 ∈ 𝑌 𝑝 ≤ ( 𝑞 ∨ 𝑟 ) } ) )
33 5 7 8 32 syl3anbr ⊢ ( ( 𝐾 ∈ 𝐵 ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ) → ( 𝑋 + 𝑌 ) = ( ( 𝑋 ∪ 𝑌 ) ∪ { 𝑝 ∈ 𝐴 ∣ ∃ 𝑞 ∈ 𝑋 ∃ 𝑟 ∈ 𝑌 𝑝 ≤ ( 𝑞 ∨ 𝑟 ) } ) )