Theorem iunocv

Description: The orthocomplement of an indexed union. (Contributed by Mario Carneiro, 23-Oct-2015)

	Ref	Expression
Hypotheses	inocv.o	⊢ ⊥ = ( ocv ‘ 𝑊 )
	iunocv.v	⊢ 𝑉 = ( Base ‘ 𝑊 )
Assertion	iunocv	⊢ ( ⊥ ‘ ∪ 𝑥 ∈ 𝐴 𝐵 ) = ( 𝑉 ∩ ∩ 𝑥 ∈ 𝐴 ( ⊥ ‘ 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		inocv.o	⊢ ⊥ = ( ocv ‘ 𝑊 )
2		iunocv.v	⊢ 𝑉 = ( Base ‘ 𝑊 )
3		iunss	⊢ ( ∪ 𝑥 ∈ 𝐴 𝐵 ⊆ 𝑉 ↔ ∀ 𝑥 ∈ 𝐴 𝐵 ⊆ 𝑉 )
4		eliun	⊢ ( 𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↔ ∃ 𝑥 ∈ 𝐴 𝑦 ∈ 𝐵 )
5	4	imbi1i	⊢ ( ( 𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 → ( 𝑧 ( ·𝑖 ‘ 𝑊 ) 𝑦 ) = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) ↔ ( ∃ 𝑥 ∈ 𝐴 𝑦 ∈ 𝐵 → ( 𝑧 ( ·𝑖 ‘ 𝑊 ) 𝑦 ) = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) )
6		r19.23v	⊢ ( ∀ 𝑥 ∈ 𝐴 ( 𝑦 ∈ 𝐵 → ( 𝑧 ( ·𝑖 ‘ 𝑊 ) 𝑦 ) = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) ↔ ( ∃ 𝑥 ∈ 𝐴 𝑦 ∈ 𝐵 → ( 𝑧 ( ·𝑖 ‘ 𝑊 ) 𝑦 ) = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) )
7	5 6	bitr4i	⊢ ( ( 𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 → ( 𝑧 ( ·𝑖 ‘ 𝑊 ) 𝑦 ) = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) ↔ ∀ 𝑥 ∈ 𝐴 ( 𝑦 ∈ 𝐵 → ( 𝑧 ( ·𝑖 ‘ 𝑊 ) 𝑦 ) = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) )
8	7	albii	⊢ ( ∀ 𝑦 ( 𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 → ( 𝑧 ( ·𝑖 ‘ 𝑊 ) 𝑦 ) = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) ↔ ∀ 𝑦 ∀ 𝑥 ∈ 𝐴 ( 𝑦 ∈ 𝐵 → ( 𝑧 ( ·𝑖 ‘ 𝑊 ) 𝑦 ) = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) )
9		df-ral	⊢ ( ∀ 𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ( 𝑧 ( ·𝑖 ‘ 𝑊 ) 𝑦 ) = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ↔ ∀ 𝑦 ( 𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 → ( 𝑧 ( ·𝑖 ‘ 𝑊 ) 𝑦 ) = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) )
10		df-ral	⊢ ( ∀ 𝑦 ∈ 𝐵 ( 𝑧 ( ·𝑖 ‘ 𝑊 ) 𝑦 ) = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ↔ ∀ 𝑦 ( 𝑦 ∈ 𝐵 → ( 𝑧 ( ·𝑖 ‘ 𝑊 ) 𝑦 ) = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) )
11	10	ralbii	⊢ ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ( 𝑧 ( ·𝑖 ‘ 𝑊 ) 𝑦 ) = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ↔ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ( 𝑦 ∈ 𝐵 → ( 𝑧 ( ·𝑖 ‘ 𝑊 ) 𝑦 ) = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) )
12		ralcom4	⊢ ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ( 𝑦 ∈ 𝐵 → ( 𝑧 ( ·𝑖 ‘ 𝑊 ) 𝑦 ) = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) ↔ ∀ 𝑦 ∀ 𝑥 ∈ 𝐴 ( 𝑦 ∈ 𝐵 → ( 𝑧 ( ·𝑖 ‘ 𝑊 ) 𝑦 ) = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) )
13	11 12	bitri	⊢ ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ( 𝑧 ( ·𝑖 ‘ 𝑊 ) 𝑦 ) = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ↔ ∀ 𝑦 ∀ 𝑥 ∈ 𝐴 ( 𝑦 ∈ 𝐵 → ( 𝑧 ( ·𝑖 ‘ 𝑊 ) 𝑦 ) = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) )
14	8 9 13	3bitr4i	⊢ ( ∀ 𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ( 𝑧 ( ·𝑖 ‘ 𝑊 ) 𝑦 ) = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ↔ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ( 𝑧 ( ·𝑖 ‘ 𝑊 ) 𝑦 ) = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) )
15	3 14	anbi12i	⊢ ( ( ∪ 𝑥 ∈ 𝐴 𝐵 ⊆ 𝑉 ∧ ∀ 𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ( 𝑧 ( ·𝑖 ‘ 𝑊 ) 𝑦 ) = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) ↔ ( ∀ 𝑥 ∈ 𝐴 𝐵 ⊆ 𝑉 ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ( 𝑧 ( ·𝑖 ‘ 𝑊 ) 𝑦 ) = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) )
16		r19.26	⊢ ( ∀ 𝑥 ∈ 𝐴 ( 𝐵 ⊆ 𝑉 ∧ ∀ 𝑦 ∈ 𝐵 ( 𝑧 ( ·𝑖 ‘ 𝑊 ) 𝑦 ) = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) ↔ ( ∀ 𝑥 ∈ 𝐴 𝐵 ⊆ 𝑉 ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ( 𝑧 ( ·𝑖 ‘ 𝑊 ) 𝑦 ) = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) )
17	15 16	bitr4i	⊢ ( ( ∪ 𝑥 ∈ 𝐴 𝐵 ⊆ 𝑉 ∧ ∀ 𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ( 𝑧 ( ·𝑖 ‘ 𝑊 ) 𝑦 ) = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) ↔ ∀ 𝑥 ∈ 𝐴 ( 𝐵 ⊆ 𝑉 ∧ ∀ 𝑦 ∈ 𝐵 ( 𝑧 ( ·𝑖 ‘ 𝑊 ) 𝑦 ) = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) )
18		eliin	⊢ ( 𝑧 ∈ 𝑉 → ( 𝑧 ∈ ∩ 𝑥 ∈ 𝐴 ( ⊥ ‘ 𝐵 ) ↔ ∀ 𝑥 ∈ 𝐴 𝑧 ∈ ( ⊥ ‘ 𝐵 ) ) )
19		eqid	⊢ ( ·𝑖 ‘ 𝑊 ) = ( ·𝑖 ‘ 𝑊 )
20		eqid	⊢ ( Scalar ‘ 𝑊 ) = ( Scalar ‘ 𝑊 )
21		eqid	⊢ ( 0g ‘ ( Scalar ‘ 𝑊 ) ) = ( 0g ‘ ( Scalar ‘ 𝑊 ) )
22	2 19 20 21 1	elocv	⊢ ( 𝑧 ∈ ( ⊥ ‘ 𝐵 ) ↔ ( 𝐵 ⊆ 𝑉 ∧ 𝑧 ∈ 𝑉 ∧ ∀ 𝑦 ∈ 𝐵 ( 𝑧 ( ·𝑖 ‘ 𝑊 ) 𝑦 ) = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) )
23		3anan12	⊢ ( ( 𝐵 ⊆ 𝑉 ∧ 𝑧 ∈ 𝑉 ∧ ∀ 𝑦 ∈ 𝐵 ( 𝑧 ( ·𝑖 ‘ 𝑊 ) 𝑦 ) = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) ↔ ( 𝑧 ∈ 𝑉 ∧ ( 𝐵 ⊆ 𝑉 ∧ ∀ 𝑦 ∈ 𝐵 ( 𝑧 ( ·𝑖 ‘ 𝑊 ) 𝑦 ) = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) ) )
24	22 23	bitri	⊢ ( 𝑧 ∈ ( ⊥ ‘ 𝐵 ) ↔ ( 𝑧 ∈ 𝑉 ∧ ( 𝐵 ⊆ 𝑉 ∧ ∀ 𝑦 ∈ 𝐵 ( 𝑧 ( ·𝑖 ‘ 𝑊 ) 𝑦 ) = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) ) )
25	24	baib	⊢ ( 𝑧 ∈ 𝑉 → ( 𝑧 ∈ ( ⊥ ‘ 𝐵 ) ↔ ( 𝐵 ⊆ 𝑉 ∧ ∀ 𝑦 ∈ 𝐵 ( 𝑧 ( ·𝑖 ‘ 𝑊 ) 𝑦 ) = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) ) )
26	25	ralbidv	⊢ ( 𝑧 ∈ 𝑉 → ( ∀ 𝑥 ∈ 𝐴 𝑧 ∈ ( ⊥ ‘ 𝐵 ) ↔ ∀ 𝑥 ∈ 𝐴 ( 𝐵 ⊆ 𝑉 ∧ ∀ 𝑦 ∈ 𝐵 ( 𝑧 ( ·𝑖 ‘ 𝑊 ) 𝑦 ) = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) ) )
27	18 26	bitr2d	⊢ ( 𝑧 ∈ 𝑉 → ( ∀ 𝑥 ∈ 𝐴 ( 𝐵 ⊆ 𝑉 ∧ ∀ 𝑦 ∈ 𝐵 ( 𝑧 ( ·𝑖 ‘ 𝑊 ) 𝑦 ) = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) ↔ 𝑧 ∈ ∩ 𝑥 ∈ 𝐴 ( ⊥ ‘ 𝐵 ) ) )
28	17 27	syl5bb	⊢ ( 𝑧 ∈ 𝑉 → ( ( ∪ 𝑥 ∈ 𝐴 𝐵 ⊆ 𝑉 ∧ ∀ 𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ( 𝑧 ( ·𝑖 ‘ 𝑊 ) 𝑦 ) = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) ↔ 𝑧 ∈ ∩ 𝑥 ∈ 𝐴 ( ⊥ ‘ 𝐵 ) ) )
29	28	pm5.32i	⊢ ( ( 𝑧 ∈ 𝑉 ∧ ( ∪ 𝑥 ∈ 𝐴 𝐵 ⊆ 𝑉 ∧ ∀ 𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ( 𝑧 ( ·𝑖 ‘ 𝑊 ) 𝑦 ) = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) ) ↔ ( 𝑧 ∈ 𝑉 ∧ 𝑧 ∈ ∩ 𝑥 ∈ 𝐴 ( ⊥ ‘ 𝐵 ) ) )
30	2 19 20 21 1	elocv	⊢ ( 𝑧 ∈ ( ⊥ ‘ ∪ 𝑥 ∈ 𝐴 𝐵 ) ↔ ( ∪ 𝑥 ∈ 𝐴 𝐵 ⊆ 𝑉 ∧ 𝑧 ∈ 𝑉 ∧ ∀ 𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ( 𝑧 ( ·𝑖 ‘ 𝑊 ) 𝑦 ) = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) )
31		3anan12	⊢ ( ( ∪ 𝑥 ∈ 𝐴 𝐵 ⊆ 𝑉 ∧ 𝑧 ∈ 𝑉 ∧ ∀ 𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ( 𝑧 ( ·𝑖 ‘ 𝑊 ) 𝑦 ) = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) ↔ ( 𝑧 ∈ 𝑉 ∧ ( ∪ 𝑥 ∈ 𝐴 𝐵 ⊆ 𝑉 ∧ ∀ 𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ( 𝑧 ( ·𝑖 ‘ 𝑊 ) 𝑦 ) = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) ) )
32	30 31	bitri	⊢ ( 𝑧 ∈ ( ⊥ ‘ ∪ 𝑥 ∈ 𝐴 𝐵 ) ↔ ( 𝑧 ∈ 𝑉 ∧ ( ∪ 𝑥 ∈ 𝐴 𝐵 ⊆ 𝑉 ∧ ∀ 𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ( 𝑧 ( ·𝑖 ‘ 𝑊 ) 𝑦 ) = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) ) )
33		elin	⊢ ( 𝑧 ∈ ( 𝑉 ∩ ∩ 𝑥 ∈ 𝐴 ( ⊥ ‘ 𝐵 ) ) ↔ ( 𝑧 ∈ 𝑉 ∧ 𝑧 ∈ ∩ 𝑥 ∈ 𝐴 ( ⊥ ‘ 𝐵 ) ) )
34	29 32 33	3bitr4i	⊢ ( 𝑧 ∈ ( ⊥ ‘ ∪ 𝑥 ∈ 𝐴 𝐵 ) ↔ 𝑧 ∈ ( 𝑉 ∩ ∩ 𝑥 ∈ 𝐴 ( ⊥ ‘ 𝐵 ) ) )
35	34	eqriv	⊢ ( ⊥ ‘ ∪ 𝑥 ∈ 𝐴 𝐵 ) = ( 𝑉 ∩ ∩ 𝑥 ∈ 𝐴 ( ⊥ ‘ 𝐵 ) )