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

Metamath Proof Explorer

Theorem paddfval

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

Ref Expression
Hypotheses paddfval.l ⊢ ≤ = ( le ‘ 𝐾 )
paddfval.j ⊢ ∨ = ( join ‘ 𝐾 )
paddfval.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
paddfval.p ⊢ + = ( +𝑃 ‘ 𝐾 )
Assertion paddfval ( 𝐾 ∈ 𝐵 → + = ( 𝑚 ∈ 𝒫 𝐴 , 𝑛 ∈ 𝒫 𝐴 ↦ ( ( 𝑚 ∪ 𝑛 ) ∪ { 𝑝 ∈ 𝐴 ∣ ∃ 𝑞 ∈ 𝑚 ∃ 𝑟 ∈ 𝑛 𝑝 ≤ ( 𝑞 ∨ 𝑟 ) } ) ) )

Proof

Step Hyp Ref Expression
1 paddfval.l ⊢ ≤ = ( le ‘ 𝐾 )
2 paddfval.j ⊢ ∨ = ( join ‘ 𝐾 )
3 paddfval.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
4 paddfval.p ⊢ + = ( +𝑃 ‘ 𝐾 )
5 elex ⊢ ( 𝐾 ∈ 𝐵 → 𝐾 ∈ V )
6 fveq2 ⊢ ( ℎ = 𝐾 → ( Atoms ‘ ℎ ) = ( Atoms ‘ 𝐾 ) )
7 6 3 eqtr4di ⊢ ( ℎ = 𝐾 → ( Atoms ‘ ℎ ) = 𝐴 )
8 7 pweqd ⊢ ( ℎ = 𝐾 → 𝒫 ( Atoms ‘ ℎ ) = 𝒫 𝐴 )
9 eqidd ⊢ ( ℎ = 𝐾 → 𝑝 = 𝑝 )
10 fveq2 ⊢ ( ℎ = 𝐾 → ( le ‘ ℎ ) = ( le ‘ 𝐾 ) )
11 10 1 eqtr4di ⊢ ( ℎ = 𝐾 → ( le ‘ ℎ ) = ≤ )
12 fveq2 ⊢ ( ℎ = 𝐾 → ( join ‘ ℎ ) = ( join ‘ 𝐾 ) )
13 12 2 eqtr4di ⊢ ( ℎ = 𝐾 → ( join ‘ ℎ ) = ∨ )
14 13 oveqd ⊢ ( ℎ = 𝐾 → ( 𝑞 ( join ‘ ℎ ) 𝑟 ) = ( 𝑞 ∨ 𝑟 ) )
15 9 11 14 breq123d ⊢ ( ℎ = 𝐾 → ( 𝑝 ( le ‘ ℎ ) ( 𝑞 ( join ‘ ℎ ) 𝑟 ) ↔ 𝑝 ≤ ( 𝑞 ∨ 𝑟 ) ) )
16 15 2rexbidv ⊢ ( ℎ = 𝐾 → ( ∃ 𝑞 ∈ 𝑚 ∃ 𝑟 ∈ 𝑛 𝑝 ( le ‘ ℎ ) ( 𝑞 ( join ‘ ℎ ) 𝑟 ) ↔ ∃ 𝑞 ∈ 𝑚 ∃ 𝑟 ∈ 𝑛 𝑝 ≤ ( 𝑞 ∨ 𝑟 ) ) )
17 7 16 rabeqbidv ⊢ ( ℎ = 𝐾 → { 𝑝 ∈ ( Atoms ‘ ℎ ) ∣ ∃ 𝑞 ∈ 𝑚 ∃ 𝑟 ∈ 𝑛 𝑝 ( le ‘ ℎ ) ( 𝑞 ( join ‘ ℎ ) 𝑟 ) } = { 𝑝 ∈ 𝐴 ∣ ∃ 𝑞 ∈ 𝑚 ∃ 𝑟 ∈ 𝑛 𝑝 ≤ ( 𝑞 ∨ 𝑟 ) } )
18 17 uneq2d ⊢ ( ℎ = 𝐾 → ( ( 𝑚 ∪ 𝑛 ) ∪ { 𝑝 ∈ ( Atoms ‘ ℎ ) ∣ ∃ 𝑞 ∈ 𝑚 ∃ 𝑟 ∈ 𝑛 𝑝 ( le ‘ ℎ ) ( 𝑞 ( join ‘ ℎ ) 𝑟 ) } ) = ( ( 𝑚 ∪ 𝑛 ) ∪ { 𝑝 ∈ 𝐴 ∣ ∃ 𝑞 ∈ 𝑚 ∃ 𝑟 ∈ 𝑛 𝑝 ≤ ( 𝑞 ∨ 𝑟 ) } ) )
19 8 8 18 mpoeq123dv ⊢ ( ℎ = 𝐾 → ( 𝑚 ∈ 𝒫 ( Atoms ‘ ℎ ) , 𝑛 ∈ 𝒫 ( Atoms ‘ ℎ ) ↦ ( ( 𝑚 ∪ 𝑛 ) ∪ { 𝑝 ∈ ( Atoms ‘ ℎ ) ∣ ∃ 𝑞 ∈ 𝑚 ∃ 𝑟 ∈ 𝑛 𝑝 ( le ‘ ℎ ) ( 𝑞 ( join ‘ ℎ ) 𝑟 ) } ) ) = ( 𝑚 ∈ 𝒫 𝐴 , 𝑛 ∈ 𝒫 𝐴 ↦ ( ( 𝑚 ∪ 𝑛 ) ∪ { 𝑝 ∈ 𝐴 ∣ ∃ 𝑞 ∈ 𝑚 ∃ 𝑟 ∈ 𝑛 𝑝 ≤ ( 𝑞 ∨ 𝑟 ) } ) ) )
20 df-padd ⊢ +𝑃 = ( ℎ ∈ V ↦ ( 𝑚 ∈ 𝒫 ( Atoms ‘ ℎ ) , 𝑛 ∈ 𝒫 ( Atoms ‘ ℎ ) ↦ ( ( 𝑚 ∪ 𝑛 ) ∪ { 𝑝 ∈ ( Atoms ‘ ℎ ) ∣ ∃ 𝑞 ∈ 𝑚 ∃ 𝑟 ∈ 𝑛 𝑝 ( le ‘ ℎ ) ( 𝑞 ( join ‘ ℎ ) 𝑟 ) } ) ) )
21 3 fvexi ⊢ 𝐴 ∈ V
22 21 pwex ⊢ 𝒫 𝐴 ∈ V
23 22 22 mpoex ⊢ ( 𝑚 ∈ 𝒫 𝐴 , 𝑛 ∈ 𝒫 𝐴 ↦ ( ( 𝑚 ∪ 𝑛 ) ∪ { 𝑝 ∈ 𝐴 ∣ ∃ 𝑞 ∈ 𝑚 ∃ 𝑟 ∈ 𝑛 𝑝 ≤ ( 𝑞 ∨ 𝑟 ) } ) ) ∈ V
24 19 20 23 fvmpt ⊢ ( 𝐾 ∈ V → ( +𝑃 ‘ 𝐾 ) = ( 𝑚 ∈ 𝒫 𝐴 , 𝑛 ∈ 𝒫 𝐴 ↦ ( ( 𝑚 ∪ 𝑛 ) ∪ { 𝑝 ∈ 𝐴 ∣ ∃ 𝑞 ∈ 𝑚 ∃ 𝑟 ∈ 𝑛 𝑝 ≤ ( 𝑞 ∨ 𝑟 ) } ) ) )
25 4 24 eqtrid ⊢ ( 𝐾 ∈ V → + = ( 𝑚 ∈ 𝒫 𝐴 , 𝑛 ∈ 𝒫 𝐴 ↦ ( ( 𝑚 ∪ 𝑛 ) ∪ { 𝑝 ∈ 𝐴 ∣ ∃ 𝑞 ∈ 𝑚 ∃ 𝑟 ∈ 𝑛 𝑝 ≤ ( 𝑞 ∨ 𝑟 ) } ) ) )
26 5 25 syl ⊢ ( 𝐾 ∈ 𝐵 → + = ( 𝑚 ∈ 𝒫 𝐴 , 𝑛 ∈ 𝒫 𝐴 ↦ ( ( 𝑚 ∪ 𝑛 ) ∪ { 𝑝 ∈ 𝐴 ∣ ∃ 𝑞 ∈ 𝑚 ∃ 𝑟 ∈ 𝑛 𝑝 ≤ ( 𝑞 ∨ 𝑟 ) } ) ) )