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	⊢ ( ( 𝐾 ∈ 𝐵 ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ) → ( 𝑋 + 𝑌 ) = ( ( 𝑋 ∪ 𝑌 ) ∪ { 𝑝 ∈ 𝐴 ∣ ∃ 𝑞 ∈ 𝑋 ∃ 𝑟 ∈ 𝑌 𝑝 ≤ ( 𝑞 ∨ 𝑟 ) } ) )