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

Metamath Proof Explorer

Theorem mat1dimbas

Description: A matrix with dimension 1 is an ordered pair with an ordered pair (of the one and only pair of indices) as first component. (Contributed by AV, 15-Aug-2019)

Ref Expression
Hypotheses mat1dim.a ⊢ 𝐴 = ( { 𝐸 } Mat 𝑅 )
mat1dim.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
mat1dim.o ⊢ 𝑂 = ⟨ 𝐸 , 𝐸 ⟩
Assertion mat1dimbas ( ( 𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉 ∧ 𝑋 ∈ 𝐵 ) → { ⟨ 𝑂 , 𝑋 ⟩ } ∈ ( Base ‘ 𝐴 ) )

Proof

Step Hyp Ref Expression
1 mat1dim.a ⊢ 𝐴 = ( { 𝐸 } Mat 𝑅 )
2 mat1dim.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
3 mat1dim.o ⊢ 𝑂 = ⟨ 𝐸 , 𝐸 ⟩
4 risset ⊢ ( 𝑋 ∈ 𝐵 ↔ ∃ 𝑟 ∈ 𝐵 𝑟 = 𝑋 )
5 eqcom ⊢ ( 𝑋 = 𝑟 ↔ 𝑟 = 𝑋 )
6 5 rexbii ⊢ ( ∃ 𝑟 ∈ 𝐵 𝑋 = 𝑟 ↔ ∃ 𝑟 ∈ 𝐵 𝑟 = 𝑋 )
7 4 6 sylbb2 ⊢ ( 𝑋 ∈ 𝐵 → ∃ 𝑟 ∈ 𝐵 𝑋 = 𝑟 )
8 7 3ad2ant3 ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉 ∧ 𝑋 ∈ 𝐵 ) → ∃ 𝑟 ∈ 𝐵 𝑋 = 𝑟 )
9 opex ⊢ ⟨ 𝐸 , 𝐸 ⟩ ∈ V
10 3 9 eqeltri ⊢ 𝑂 ∈ V
11 simp3 ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉 ∧ 𝑋 ∈ 𝐵 ) → 𝑋 ∈ 𝐵 )
12 opthg ⊢ ( ( 𝑂 ∈ V ∧ 𝑋 ∈ 𝐵 ) → ( ⟨ 𝑂 , 𝑋 ⟩ = ⟨ 𝑂 , 𝑟 ⟩ ↔ ( 𝑂 = 𝑂 ∧ 𝑋 = 𝑟 ) ) )
13 10 11 12 sylancr ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉 ∧ 𝑋 ∈ 𝐵 ) → ( ⟨ 𝑂 , 𝑋 ⟩ = ⟨ 𝑂 , 𝑟 ⟩ ↔ ( 𝑂 = 𝑂 ∧ 𝑋 = 𝑟 ) ) )
14 opex ⊢ ⟨ 𝑂 , 𝑋 ⟩ ∈ V
15 sneqbg ⊢ ( ⟨ 𝑂 , 𝑋 ⟩ ∈ V → ( { ⟨ 𝑂 , 𝑋 ⟩ } = { ⟨ 𝑂 , 𝑟 ⟩ } ↔ ⟨ 𝑂 , 𝑋 ⟩ = ⟨ 𝑂 , 𝑟 ⟩ ) )
16 14 15 ax-mp ⊢ ( { ⟨ 𝑂 , 𝑋 ⟩ } = { ⟨ 𝑂 , 𝑟 ⟩ } ↔ ⟨ 𝑂 , 𝑋 ⟩ = ⟨ 𝑂 , 𝑟 ⟩ )
17 eqid ⊢ 𝑂 = 𝑂
18 17 biantrur ⊢ ( 𝑋 = 𝑟 ↔ ( 𝑂 = 𝑂 ∧ 𝑋 = 𝑟 ) )
19 13 16 18 3bitr4g ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉 ∧ 𝑋 ∈ 𝐵 ) → ( { ⟨ 𝑂 , 𝑋 ⟩ } = { ⟨ 𝑂 , 𝑟 ⟩ } ↔ 𝑋 = 𝑟 ) )
20 19 rexbidv ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉 ∧ 𝑋 ∈ 𝐵 ) → ( ∃ 𝑟 ∈ 𝐵 { ⟨ 𝑂 , 𝑋 ⟩ } = { ⟨ 𝑂 , 𝑟 ⟩ } ↔ ∃ 𝑟 ∈ 𝐵 𝑋 = 𝑟 ) )
21 8 20 mpbird ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉 ∧ 𝑋 ∈ 𝐵 ) → ∃ 𝑟 ∈ 𝐵 { ⟨ 𝑂 , 𝑋 ⟩ } = { ⟨ 𝑂 , 𝑟 ⟩ } )
22 1 2 3 mat1dimelbas ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉 ) → ( { ⟨ 𝑂 , 𝑋 ⟩ } ∈ ( Base ‘ 𝐴 ) ↔ ∃ 𝑟 ∈ 𝐵 { ⟨ 𝑂 , 𝑋 ⟩ } = { ⟨ 𝑂 , 𝑟 ⟩ } ) )
23 22 3adant3 ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉 ∧ 𝑋 ∈ 𝐵 ) → ( { ⟨ 𝑂 , 𝑋 ⟩ } ∈ ( Base ‘ 𝐴 ) ↔ ∃ 𝑟 ∈ 𝐵 { ⟨ 𝑂 , 𝑋 ⟩ } = { ⟨ 𝑂 , 𝑟 ⟩ } ) )
24 21 23 mpbird ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉 ∧ 𝑋 ∈ 𝐵 ) → { ⟨ 𝑂 , 𝑋 ⟩ } ∈ ( Base ‘ 𝐴 ) )