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	syl5eq	⊢ ( 𝐾 ∈ V → + = ( 𝑚 ∈ 𝒫 𝐴 , 𝑛 ∈ 𝒫 𝐴 ↦ ( ( 𝑚 ∪ 𝑛 ) ∪ { 𝑝 ∈ 𝐴 ∣ ∃ 𝑞 ∈ 𝑚 ∃ 𝑟 ∈ 𝑛 𝑝 ≤ ( 𝑞 ∨ 𝑟 ) } ) ) )
26	5 25	syl	⊢ ( 𝐾 ∈ 𝐵 → + = ( 𝑚 ∈ 𝒫 𝐴 , 𝑛 ∈ 𝒫 𝐴 ↦ ( ( 𝑚 ∪ 𝑛 ) ∪ { 𝑝 ∈ 𝐴 ∣ ∃ 𝑞 ∈ 𝑚 ∃ 𝑟 ∈ 𝑛 𝑝 ≤ ( 𝑞 ∨ 𝑟 ) } ) ) )